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