# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1489416733 0
# Node ID 05fa26637da462e2a2848791260451bfc306a317
# Parent  f476c98cad28eefc26f4d0cc2f8430353efd2623
updated

diff -r f476c98cad28 -r 05fa26637da4 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Mar 11 19:33:38 2017 +0000
+++ b/thys/LexerExt.thy	Mon Mar 13 14:52:13 2017 +0000
@@ -777,11 +777,11 @@
     \<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 (UPNTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"
-| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; 
+| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<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 (NTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []"
-| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; 
+| Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<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 (FROMNTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow>  s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs"
@@ -1115,14 +1115,13 @@
   then show "Stars [] = v2" by cases (auto simp add: Posix1)
 next
   case (Posix_NTIMES1 s1 r v s2 n vs v2)
-  have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" 
+  have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2"  "flat v = [] \<Longrightarrow> flat (Stars vs) = []"
        "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<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 r \<and> s\<^sub>4 \<in> L (NTIMES r n))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
-  apply (metis Posix1(1) Posix_NTIMES1.hyps(5) append_Nil append_Nil2)
-  done  
+  by (metis Posix1(1) Posix_NTIMES1.hyps(6) append_Nil append_Nil2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1138,12 +1137,12 @@
 next
   case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
   have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs"
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<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 (FROMNTIMES r n))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
-  by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2)
+  by (metis Posix1(1) Posix_FROMNTIMES1.hyps(6) append_Nil append_Nil2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1431,7 +1430,7 @@
   then consider
       (cons) m v1 vs s1 s2 where 
         "n = Suc m"
-        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []"
         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<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 (NTIMES r m))" 
         apply(case_tac n)
@@ -1448,6 +1447,8 @@
           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 "flat v = [] \<Longrightarrow> flat (Stars vs) = []" by fact
+        moreover
           have "s2 \<in> NTIMES r m \<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 (NTIMES r m))" by fact
@@ -1457,7 +1458,7 @@
         have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" 
           apply(rule_tac Posix.intros(10))
           apply(simp_all)
-          done
+          by (simp add: Posix1(2))
         then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp)
     qed
 next 
@@ -1472,7 +1473,7 @@
         "\<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 (FROMNTIMES r 0))" 
       | (cons) m v1 vs s1 s2 where 
         "n = Suc m"
-        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []"
         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<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 (FROMNTIMES r m))" 
         apply(case_tac n)
@@ -1494,6 +1495,8 @@
           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
         moreover
           have "s2 \<in> FROMNTIMES r m \<rightarrow> Stars vs" by fact
+        moreover
+          have "flat v = [] \<Longrightarrow> flat (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 (FROMNTIMES r m))" 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 (FROMNTIMES r m))" 
@@ -1501,8 +1504,8 @@
         ultimately 
         have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" 
           apply(rule_tac Posix.intros(12))
-          apply(simp_all)
-          done
+          apply(simp_all) 
+          by (simp add: Posix1(2))
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
       next
       case null