# HG changeset patch
# User cu
# Date 1507468884 -3600
# Node ID 42268a284ea6274b7327a30c371099bf5c0a91ab
# Parent  a3134f7de0654036b1387c8021929a10f44bc1c9
updated

diff -r a3134f7de065 -r 42268a284ea6 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/LexerExt.thy	Sun Oct 08 14:21:24 2017 +0100
@@ -170,7 +170,6 @@
      apply(simp add: Prf_injval_flat)
      apply(simp)
    apply(simp)
-  using Prf.intros(10) Prf_injval_flat apply auto
 done
 
 
@@ -190,15 +189,6 @@
       apply(auto)
   done
     
-lemma test:
-  assumes "s \<in> der c (FROMNTIMES r 0) \<rightarrow> v"
-  shows "XXX"
-using assms    
-  apply(simp)
-  apply(erule Posix_elims)
-  apply(drule FROMNTIMES_0)
-  apply(auto)
-oops    
 
 lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v" 
@@ -454,18 +444,15 @@
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n"
         "\<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 (n - 1)))"
-     | (null)  v1 where 
-        "v = Seq v1 (Stars [])"  
-        "s \<in> der c r \<rightarrow> v1" "[] \<in> (FROMNTIMES r 0) \<rightarrow> (Stars [])" "n = 0"
+     | (null) v1 vs s1 s2 where 
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2"  "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" 
+        "s1 \<in> der c r \<rightarrow> v1" "n = 0"
+         "\<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))"
     (* here *)    
     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
+    prefer 2
     apply(erule Posix_elims)
     apply(simp)
-    apply(case_tac "n = 0")
-     apply(simp)
-     apply(drule FROMNTIMES_0)
-     apply(simp)
-    using FROMNTIMES_0 Posix_mkeps apply force
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
     apply(drule_tac x="v1" in meta_spec)
@@ -473,13 +460,22 @@
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
      apply(simp add: der_correctness Der_def)
-     apply(case_tac "n = 0")
-      apply(simp)
-      apply(simp)
-      apply(rotate_tac 4)
+      apply(rotate_tac 5)
     apply(erule Posix_elims)
       apply(auto)[2]
-      done
+    apply(erule Posix_elims)
+      apply(simp)
+     apply blast
+    apply(erule Posix_elims)
+    apply(auto)
+      apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)      
+    apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
+     apply(clarify)
+    apply simp
+      apply(rotate_tac 6)
+    apply(erule Posix_elims)
+      apply(auto)[2]
+    done
     then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v" 
     proof (cases)
       case cons
@@ -508,27 +504,27 @@
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp)
       next 
        case null
-          have "s \<in> der c r \<rightarrow> v1" by fact
-          then have "(c # s) \<in> r \<rightarrow> injval r c v1" using IH by simp
-        moreover
-          have "[] \<in> (FROMNTIMES r 0) \<rightarrow> Stars []" by fact
-        moreover 
-          have "(c # s) \<in> r \<rightarrow> injval r c v1" by fact 
-          then have "flat (injval r c v1) = (c # s)" by (rule Posix1)
+          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 "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
+          then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
           then have "flat (injval r c v1) \<noteq> []" by simp
+          moreover
+             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 # s) @ []) \<in> FROMNTIMES r 1 \<rightarrow> Stars [injval r c v1]" 
-           apply (rule_tac Posix.intros)
-              apply(simp_all)
+        have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" 
+           apply (rule_tac Posix.intros) back
+             apply(simp_all)
            done
         then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null 
           apply(simp)
-          apply(erule Posix_elims)
-           apply(auto)
-           apply(rotate_tac 6) 
-          apply(drule FROMNTIMES_0)
-          apply(simp)  
-            sorry
+          done  
       qed  
   next
     case (NMTIMES x1 x2 m s v)
diff -r a3134f7de065 -r 42268a284ea6 thys/PositionsExt.thy
--- a/thys/PositionsExt.thy	Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/PositionsExt.thy	Sun Oct 08 14:21:24 2017 +0100
@@ -889,7 +889,55 @@
       then show "Stars (v # vs) :\<sqsubseteq>val v3"
       unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
-  qed         
+  qed        
+next    
+  case (Posix_FROMNTIMES3 s1 r v s2 vs v3)
+      have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
+  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
+  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  have cond: "\<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
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (FROMNTIMES r 0) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
+    "flat (Stars (v3a # vs3)) = s1 @ s2"
+  | (Empty) "v3 = Stars []" 
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf.cases)
+  apply(auto)
+  apply(case_tac vs)
+  apply(auto intro: Prf.intros)
+  done
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 
+      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+        by (simp add: sprefix_list_def append_eq_conv_conj)
+      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
+        using PosOrd_spreI as1(1) NonEmpty(4) by blast
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 
+        using NonEmpty(2,3) by (auto simp add: LV_def)
+      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
+         unfolding PosOrd_ex_eq_def by auto     
+      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+        unfolding  PosOrd_ex_eq_def
+        using PosOrd_StarsI PosOrd_StarsI2 by auto 
+      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+    next 
+      case Empty
+      have "v3 = Stars []" by fact
+      then show "Stars (v # vs) :\<sqsubseteq>val v3"
+      unfolding PosOrd_ex_eq_def using cond2
+      by (simp add: PosOrd_shorterI)
+    qed      
 next
   case (Posix_NMTIMES2 vs r n m v2) 
   then show "Stars vs :\<sqsubseteq>val v2" sorry
diff -r a3134f7de065 -r 42268a284ea6 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/SpecExt.thy	Sun Oct 08 14:21:24 2017 +0100
@@ -272,7 +272,10 @@
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))"
 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))"
-| "der c (FROMNTIMES r n) = SEQ (der c r) (FROMNTIMES r (n - 1))"
+| "der c (FROMNTIMES r n) = 
+     (if n = 0 
+      then SEQ (der c r) (STAR r)
+      else SEQ (der c r) (FROMNTIMES r (n - 1)))"
 | "der c (NMTIMES r n m) = 
      (if m < n then ZERO 
       else (if n = 0 then (if m = 0 then ZERO else 
@@ -314,6 +317,8 @@
     apply(simp)
 (* FROMNTIMES *)    
    apply(simp add: nullable_correctness del: Der_UNION)
+  apply(rule conjI)
+prefer 2    
 apply(subst Sequ_Union_in)
 apply(subst Der_Pow_Sequ[symmetric])
 apply(subst Pow.simps[symmetric])
@@ -322,12 +327,10 @@
 apply(subst Pow_Sequ_Un2)
 apply(simp)
 apply(simp)
-apply(auto simp add: Sequ_def Der_def)[1]
-apply(rule_tac x="Suc xa" in exI)
-apply(auto simp add: Sequ_def)[1]
-apply(drule Pow_decomp)
-apply(auto)[1]
-   apply (metis append_Cons)
+    apply(auto simp add: Sequ_def Der_def)[1]
+   apply(auto simp add: Sequ_def split: if_splits)[1]
+  using Star_Pow apply fastforce
+  using Pow_Star apply blast
 (* NMTIMES *)    
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(rule impI)
@@ -1165,6 +1168,9 @@
 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n;
     \<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 - 1)))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)"  
+| Posix_FROMNTIMES3: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+    \<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> FROMNTIMES r 0 \<rightarrow> Stars (v # vs)"  
 | Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk>
     \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs"  
 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m;
@@ -1205,6 +1211,7 @@
        apply(rule_tac x="Suc x" in bexI)
         apply(simp add: Sequ_def)
           apply(auto)[3]
+    defer
      apply(simp)
   apply fastforce
     apply(simp)
@@ -1213,7 +1220,8 @@
    apply(rule_tac x="Suc x" in bexI)
     apply(auto simp add: Sequ_def)[2]
    apply(simp)
-done  
+  apply(simp)
+  by (simp add: Star.step Star_Pow)
   
 text {*
   Our Posix definition determines a unique value.
@@ -1343,22 +1351,21 @@
 next
   case (Posix_FROMNTIMES1 s1 r v s2 n vs v2)
   have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []"
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" "0 < n"
        "\<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 - 1 )))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
     using Posix1(1) Posix1(2) apply blast 
-    apply(drule_tac x="v" in meta_spec)
-    apply(drule_tac x="vs" in meta_spec)
-    apply(simp)
-    apply(drule meta_mp)
      apply(case_tac n)
       apply(simp)
-      apply(rule conjI)      
-     apply (smt L.simps(9) One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps Suc_mono Suc_pred UN_E append.right_neutral append_Nil lessI less_antisym list.size(3) nat.simps(3) neq0_conv not_less_eq val.inject(5))
-       apply(rule List_eq_zipI)
-        apply(auto)[1]
-    sorry  
+      apply(simp)
+    apply(drule_tac x="va" in meta_spec)
+    apply(drule_tac x="vs" in meta_spec)
+    apply(simp)
+     apply(drule meta_mp)
+    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
+    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
+    by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1370,9 +1377,24 @@
      apply(auto)
     apply(rule List_eq_zipI)
      apply(auto)
-     apply(meson in_set_zipE)
-    by (simp add: Posix1(2))
+      apply(meson in_set_zipE)
+     apply (simp add: Posix1(2))
+    using Posix1(2) by blast
 next
+  case (Posix_FROMNTIMES3 s1 r v s2 vs v2)  
+    have "(s1 @ s2) \<in> FROMNTIMES r 0 \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []"
+       "\<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(2) apply fastforce
+    using Posix1(1) apply fastforce
+    by (metis Posix1(1) Posix_FROMNTIMES3.hyps(6) append.right_neutral append_Nil)
+  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+
+  ultimately show "Stars (v # vs) = v2" by auto     
+next    
   case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
   then show "Stars (v # vs) = v2"
     sorry
@@ -1397,55 +1419,31 @@
   defer
      apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
   apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
-  prefer 4
-  apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[1]
-   apply(subst append.simps(2)[symmetric])
-  apply(rule Prf.intros)
-    apply(auto)
-  prefer 4
-  apply (metis Prf.intros(8) append_Nil empty_iff list.set(1))
-  apply(erule Posix_elims)
-  apply(auto)
-  apply(rule_tac t="v # vsa" and s = "[v] @ vsa" in subst)
-  apply(simp)
-  apply(rule Prf.intros)
-   apply(simp)
-  apply(auto)[1]
-  apply(auto simp add: Sequ_def intro: Prf.intros elim: Prf_elims)[1]
-  apply(simp)
-  apply(rotate_tac 4)
-  apply(erule Prf_elims)
-    apply(auto)
-   apply(case_tac n)
-  apply(simp)
-  
+     apply(simp)
+     apply(clarify)
+     apply(case_tac n)
+      apply(simp)
+     apply(simp)
+     apply(erule Prf_elims)
+      apply(simp)
   apply(subst append.simps(2)[symmetric])
-  apply(rule Prf.intros)
-   apply(auto)
-  apply(rule Prf.intros(10))
-   apply(auto)
-  apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
-  apply(rotate_tac 6)
-  apply(erule Prf_elims)
-  apply(simp)
-  apply(subst append.simps(2)[symmetric])
-  apply(rule Prf.intros)
-    apply(auto)
-  apply(rule_tac t="v # vsa" and s = "(v # vsa) @ []" in subst)
-  apply(simp)
-  apply(simp add: Prf.intros(12))
-  done
+      apply(rule Prf.intros) 
+        apply(simp)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+     apply(rule Prf.intros)  
+      apply(simp)
+     apply(simp)
+    apply(simp)
+   apply(clarify)
+   apply(erule Prf_elims)
+      apply(simp)
+  apply(rule Prf.intros)  
+       apply(simp)
+    apply(simp)
+  (* NMTIMES *)
+  sorry
     
-lemma FROMNTIMES_0:
-  assumes "s \<in> FROMNTIMES r 0 \<rightarrow> v"
-  shows "s = [] \<and> v = Stars []"
-  using assms
-  apply(erule_tac Posix_elims)
-   apply(auto)
-  done    
-    
-lemma FROMNTIMES_der_0:
-  shows "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
-by(simp)    
   
 end
\ No newline at end of file