diff -r deea42c83c9e -r a3134f7de065 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Thu Oct 05 12:45:13 2017 +0100
+++ b/thys/SpecExt.thy	Sat Oct 07 22:16:16 2017 +0100
@@ -311,8 +311,9 @@
 apply(subst Pow_Sequ_Un)
 apply(simp)
 apply(simp only: Der_union Der_empty)
-apply(simp)
-apply(simp add: nullable_correctness del: Der_UNION)
+    apply(simp)
+(* FROMNTIMES *)    
+   apply(simp add: nullable_correctness del: Der_UNION)
 apply(subst Sequ_Union_in)
 apply(subst Der_Pow_Sequ[symmetric])
 apply(subst Pow.simps[symmetric])
@@ -326,7 +327,8 @@
 apply(auto simp add: Sequ_def)[1]
 apply(drule Pow_decomp)
 apply(auto)[1]
-apply (metis append_Cons)
+   apply (metis append_Cons)
+(* NMTIMES *)    
 apply(simp add: nullable_correctness del: Der_UNION)
 apply(rule impI)
 apply(rule conjI)
@@ -663,10 +665,10 @@
   case (FROMNTIMES r n)
   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
   have "s \<in> L (FROMNTIMES r n)" by fact 
-  then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m"  "n \<le> m"
+  then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k"  "n \<le> k"
     "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"
     using Pow_cstring by force 
-  then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m"
+  then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k"
       "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"
   using IH flats_cval 
   apply -
@@ -723,11 +725,26 @@
   apply(simp)
   done
   then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s"
-  apply(rule_tac x="Stars (vs1 @ vs2)" in exI)
+    apply(case_tac "length vs1 \<le> n")
+  apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)
   apply(simp)
-  apply(rule Prf.intros)
-       apply(auto) 
-  sorry
+  apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")
+  prefer 2
+  apply (meson flats_empty in_set_takeD)
+  apply(clarify)
+    apply(rule conjI)
+      apply(rule Prf.intros)
+        apply(simp)
+       apply (meson in_set_takeD)
+      apply(simp)
+     apply(simp)
+     apply (simp add: flats_empty)
+      apply(rule_tac x="Stars vs1" in exI)
+  apply(simp)
+    apply(rule conjI)
+     apply(rule Prf.intros)
+      apply(auto)
+  done    
 next 
   case (UPNTIMES r n s)
   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
@@ -806,6 +823,58 @@
   ultimately show "finite (Prefixes s)" by simp
 qed
 
+definition
+  "Stars_Cons V Vs \<equiv> {Stars (v # vs) | v vs. v \<in> V \<and> Stars vs \<in> Vs}"
+  
+definition
+  "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}"
+
+fun Stars_Pow :: "val set \<Rightarrow> nat \<Rightarrow> val set"
+where  
+  "Stars_Pow Vs 0 = {Stars []}"
+| "Stars_Pow Vs (Suc n) = Stars_Cons Vs (Stars_Pow Vs n)"
+  
+lemma finite_Stars_Cons:
+  assumes "finite V" "finite Vs"
+  shows "finite (Stars_Cons V Vs)"
+  using assms  
+proof -
+  from assms(2) have "finite (Stars -` Vs)"
+    by(simp add: finite_vimageI inj_on_def) 
+  with assms(1) have "finite (V \<times> (Stars -` Vs))"
+    by(simp)
+  then have "finite ((\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs)))"
+    by simp
+  moreover have "Stars_Cons V Vs = (\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs))"
+    unfolding Stars_Cons_def by auto    
+  ultimately show "finite (Stars_Cons V Vs)"   
+    by simp
+qed
+
+lemma finite_Stars_Append:
+  assumes "finite Vs1" "finite Vs2"
+  shows "finite (Stars_Append Vs1 Vs2)"
+  using assms  
+proof -
+  define UVs1 where "UVs1 \<equiv> Stars -` Vs1"
+  define UVs2 where "UVs2 \<equiv> Stars -` Vs2"  
+  from assms have "finite UVs1" "finite UVs2"
+    unfolding UVs1_def UVs2_def
+    by(simp_all add: finite_vimageI inj_on_def) 
+  then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))"
+    by simp
+  moreover 
+    have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)"
+    unfolding Stars_Append_def UVs1_def UVs2_def by auto    
+  ultimately show "finite (Stars_Append Vs1 Vs2)"   
+    by simp
+qed 
+ 
+lemma finite_Stars_Pow:
+  assumes "finite Vs"
+  shows "finite (Stars_Pow Vs n)"    
+by (induct n) (simp_all add: finite_Stars_Cons assms)
+    
 lemma LV_STAR_finite:
   assumes "\<forall>s. finite (LV r s)"
   shows "finite (LV (STAR r) s)"
@@ -816,18 +885,20 @@
     by (auto simp add: strict_suffix_def) 
   define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
-  define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
+  define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2"
   have "finite S1" using assms
     unfolding S1_def by (simp_all add: finite_Prefixes)
   moreover 
   with IH have "finite S2" unfolding S2_def
-    by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
+    by (auto simp add: finite_SSuffixes)
   ultimately 
-  have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
+  have "finite ({Stars []} \<union> Stars_Cons S1 S2)" 
+    by (simp add: finite_Stars_Cons)
   moreover 
-  have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
-  unfolding S1_def S2_def f_def
-  unfolding LV_def image_def prefix_def strict_suffix_def
+  have "LV (STAR r) s \<subseteq> {Stars []} \<union> (Stars_Cons S1 S2)" 
+  unfolding S1_def S2_def f_def LV_def Stars_Cons_def
+  unfolding prefix_def strict_suffix_def 
+  unfolding image_def
   apply(auto)
   apply(case_tac x)
   apply(auto elim: Prf_elims)
@@ -837,12 +908,12 @@
   apply(auto intro: Prf.intros)  
   apply(rule exI)
   apply(rule conjI)
-  apply(rule_tac x="flat a" in exI)
+  apply(rule_tac x="flats list" in exI)
   apply(rule conjI)
-  apply(rule_tac x="flats list" in exI)
+  apply(rule_tac x="flat a" in exI)
   apply(simp)
   apply(blast)
-  using Prf.intros(6) by blast  
+  using Prf.intros(6) flat_Stars by blast  
   ultimately
   show "finite (LV (STAR r) s)" by (simp add: finite_subset)
 qed  
@@ -851,37 +922,6 @@
   "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s"
 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims)
 
-
-lemma LV_NTIMES_0:
-  shows "LV (NTIMES r 0) s \<subseteq> {Stars []}"
-unfolding LV_def
-apply(auto elim: Prf_elims)
-done
-
-lemma LV_NTIMES_1:
-  shows "LV (NTIMES r 1) s \<subseteq> (\<lambda>v. Stars [v]) ` (LV r s)"
-unfolding LV_def
-apply(auto elim!: Prf_elims)
-apply(case_tac vs1)
-apply(simp)
-apply(case_tac vs2)
-apply(simp)
-apply(simp)
-apply(simp)
-done
-
-lemma LV_NTIMES_2:
-  shows "LV (NTIMES r 2) [] \<subseteq> (\<lambda>(v1,v2). Stars [v1,v2]) ` (LV r [] \<times> LV r [])"
-unfolding LV_def
-apply(auto elim!: Prf_elims simp add: image_def)
-apply(case_tac vs1)
-apply(auto)
-apply(case_tac vs2)
-apply(auto)
-apply(case_tac list)
-apply(auto)
-done
-
 lemma LV_NTIMES_3:
   shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))"
 unfolding LV_def
@@ -896,66 +936,147 @@
 apply(subst append.simps(1)[symmetric])
 apply(rule Prf.intros)
 apply(auto)
-done
-
-thm card_cartesian_product
-
-lemma finite_list:
-  assumes "finite A"
-  shows "finite {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n}"
-  apply(induct n)
-   apply(simp)
-   apply (smt Collect_cong empty_iff finite.emptyI finite.insertI 
-   in_listsI list.set(1) lists_empty mem_Collect_eq singleton_conv2)
-  apply(rule_tac B="{[]} \<union> (\<lambda>(v,vs). v # vs) `(A \<times> {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n})" in finite_subset)  
-   apply(auto simp add: image_def)[1]
-   apply(case_tac x)
-    apply(simp)
-   apply(simp)
-  apply(simp)
-  apply(rule finite_imageI)
-    using assms
-    apply(simp)
-    done
-      
-lemma test:
-  "LV (NTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
-apply(auto simp add: LV_def elim: Prf_elims)
-done
+  done 
     
-lemma test3:
-  "LV (FROMNTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
-  apply(auto simp add: image_def LV_def elim!: Prf_elims)
-   apply blast
-  apply(case_tac vs)
+lemma LV_FROMNTIMES_3:
+  shows "LV (FROMNTIMES r (Suc n)) [] = 
+    (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (FROMNTIMES r n) [])))"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+     apply(auto)
+  apply (metis le_imp_less_Suc length_greater_0_conv less_antisym list.exhaust list.set_intros(1) not_less_eq zero_le)
+  prefer 2
+  using nth_mem apply blast
+  apply(case_tac vs1)
+  apply (smt Groups.add_ac(2) Prf.intros(9) add.right_neutral add_Suc_right append.simps(1) insert_iff length_append list.set(2) list.size(3) list.size(4))
     apply(auto)
-  done   
-    
-    
+done     
+  
+lemma LV_NTIMES_4:
+ "LV (NTIMES r n) [] = Stars_Pow (LV r []) n" 
+  apply(induct n)
+   apply(simp add: LV_def)    
+   apply(auto elim!: Prf_elims simp add: image_def)[1]
+   apply(subst append.simps[symmetric])
+    apply(rule Prf.intros)
+      apply(simp_all)
+    apply(simp add: LV_NTIMES_3 image_def Stars_Cons_def)
+  apply blast
+ done   
 
-lemma LV_NTIMES_empty_finite:
-  assumes "finite (LV r [])"
-  shows "finite (LV (NTIMES r n) [])"
-  using assms
-  apply -  
+lemma LV_NTIMES_5:
+  "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+  apply(auto simp add: Stars_Append_def)
+  apply(rule_tac x="vs1" in exI)
+  apply(rule_tac x="vs2" in exI)  
+  apply(auto)
+    using Prf.intros(6) apply(auto)
+      apply(rule_tac x="length vs2" in bexI)
+    thm Prf.intros
+      apply(subst append.simps(1)[symmetric])
+    apply(rule Prf.intros)
+      apply(auto)[1]
+      apply(auto)[1]
+     apply(simp)
+    apply(simp)
+      done
+      
+lemma ttty:
+ "LV (FROMNTIMES r n) [] = Stars_Pow (LV r []) n" 
+  apply(induct n)
+   apply(simp add: LV_def)    
+   apply(auto elim: Prf_elims simp add: image_def)[1]
+   prefer 2
+    apply(subst append.simps[symmetric])
+    apply(rule Prf.intros)
+      apply(simp_all)
+   apply(erule Prf_elims) 
+    apply(case_tac vs1)
+     apply(simp)
+    apply(simp)
+   apply(case_tac x)
+    apply(simp_all)
+    apply(simp add: LV_FROMNTIMES_3 image_def Stars_Cons_def)
+  apply blast
+ done     
+
+lemma LV_FROMNTIMES_5:
+  "LV (FROMNTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+  apply(auto simp add: Stars_Append_def)
+  apply(rule_tac x="vs1" in exI)
+  apply(rule_tac x="vs2" in exI)  
+  apply(auto)
+    using Prf.intros(6) apply(auto)
+      apply(rule_tac x="length vs2" in bexI)
+    thm Prf.intros
+      apply(subst append.simps(1)[symmetric])
+    apply(rule Prf.intros)
+      apply(auto)[1]
+      apply(auto)[1]
+     apply(simp)
+     apply(simp)
+      apply(rule_tac x="vs" in exI)
+    apply(rule_tac x="[]" in exI) 
+    apply(auto)
+    by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le)
+
+lemma LV_FROMNTIMES_6:
+  assumes "\<forall>s. finite (LV r s)"
+  shows "finite (LV (FROMNTIMES r n) s)"
   apply(rule finite_subset)
-   apply(rule test)
-  apply(rule finite_imageI)
-    apply(rule finite_list)
-   apply(simp)
-  done
+   apply(rule LV_FROMNTIMES_5)
+  apply(rule finite_Stars_Append)
+    apply(rule LV_STAR_finite)
+   apply(rule assms)
+  apply(rule finite_UN_I)
+   apply(auto)
+  by (simp add: assms finite_Stars_Pow ttty)
     
-lemma LV_NTIMES_STAR:
-  "LV (NTIMES r n) s \<subseteq> LV (STAR r) s"
-apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
-apply(rule Prf.intros)
-oops
+lemma LV_NMTIMES_5:
+  "LV (NMTIMES r n m) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES r i) [])"
+apply(auto simp add: LV_def)
+apply(auto elim!: Prf_elims)
+  apply(auto simp add: Stars_Append_def)
+  apply(rule_tac x="vs1" in exI)
+  apply(rule_tac x="vs2" in exI)  
+  apply(auto)
+    using Prf.intros(6) apply(auto)
+      apply(rule_tac x="length vs2" in bexI)
+    thm Prf.intros
+      apply(subst append.simps(1)[symmetric])
+    apply(rule Prf.intros)
+      apply(auto)[1]
+      apply(auto)[1]
+     apply(simp)
+     apply(simp)
+      apply(rule_tac x="vs" in exI)
+    apply(rule_tac x="[]" in exI) 
+    apply(auto)
+    by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le)
 
-lemma LV_FROMNTIMES_STAR:
-  "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s"
-apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
-oops
-
+lemma LV_NMTIMES_6:
+  assumes "\<forall>s. finite (LV r s)"
+  shows "finite (LV (NMTIMES r n m) s)"
+  apply(rule finite_subset)
+   apply(rule LV_NMTIMES_5)
+  apply(rule finite_Stars_Append)
+    apply(rule LV_STAR_finite)
+   apply(rule assms)
+  apply(rule finite_UN_I)
+   apply(auto)
+  by (simp add: assms finite_Stars_Pow ttty)
+        
+    
 lemma LV_finite:
   shows "finite (LV r s)"
 proof(induct r arbitrary: s)
@@ -999,7 +1120,17 @@
   case (FROMNTIMES r n s)
   have "\<And>s. finite (LV r s)" by fact
   then show "finite (LV (FROMNTIMES r n) s)"
-  
+    by (simp add: LV_FROMNTIMES_6)
+next 
+  case (NTIMES r n s)
+  have "\<And>s. finite (LV r s)" by fact
+  then show "finite (LV (NTIMES r n) s)"
+    by (metis (no_types, lifting) LV_NTIMES_4 LV_NTIMES_5 LV_STAR_finite finite_Stars_Append finite_Stars_Pow finite_UN_I finite_atMost finite_subset)
+next
+  case (NMTIMES r n m s)
+  have "\<And>s. finite (LV r s)" by fact
+  then show "finite (LV (NMTIMES r n m) s)"
+    by (simp add: LV_NMTIMES_6)         
 qed
 
 
@@ -1020,7 +1151,26 @@
     \<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> STAR r \<rightarrow> Stars (v # vs)"
 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
-
+| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES 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 (NTIMES r (n - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
+    \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs"  
+| Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES 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 (UPNTIMES r (n - 1)))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r n \<rightarrow> Stars (v # vs)"
+| Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"
+| Posix_FROMNTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk>
+    \<Longrightarrow> [] \<in> FROMNTIMES r n \<rightarrow> Stars vs"
+| 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_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;
+    \<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)"  
+  
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
@@ -1028,17 +1178,60 @@
   "s \<in> ALT r1 r2 \<rightarrow> v"
   "s \<in> SEQ r1 r2 \<rightarrow> v"
   "s \<in> STAR r \<rightarrow> v"
-
+  "s \<in> NTIMES r n \<rightarrow> v"
+  "s \<in> UPNTIMES r n \<rightarrow> v"
+  "s \<in> FROMNTIMES r n \<rightarrow> v"
+  "s \<in> NMTIMES r n m \<rightarrow> v"
+  
 lemma Posix1:
   assumes "s \<in> r \<rightarrow> v"
   shows "s \<in> L r" "flat v = s"
 using assms
-by (induct s r v rule: Posix.induct)
-   (auto simp add: Sequ_def)
-
+  apply(induct s r v rule: Posix.induct)
+                    apply(auto simp add: Sequ_def)[18]
+            apply(case_tac n)
+             apply(simp)
+  apply(simp add: Sequ_def)
+            apply(auto)[1]
+           apply(simp)
+  apply(clarify)
+  apply(rule_tac x="Suc x" in bexI)
+  apply(simp add: Sequ_def)
+            apply(auto)[5]
+  using nth_mem nullable.simps(9) nullable_correctness apply auto[1]
+  apply simp
+       apply(simp)
+       apply(clarify)
+       apply(rule_tac x="Suc x" in bexI)
+        apply(simp add: Sequ_def)
+          apply(auto)[3]
+     apply(simp)
+  apply fastforce
+    apply(simp)
+   apply(simp)
+    apply(clarify)
+   apply(rule_tac x="Suc x" in bexI)
+    apply(auto simp add: Sequ_def)[2]
+   apply(simp)
+done  
+  
 text {*
   Our Posix definition determines a unique value.
 *}
+  
+lemma List_eq_zipI:
+  assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 = v2" 
+  and "length vs1 = length vs2"
+  shows "vs1 = vs2"  
+ using assms
+  apply(induct vs1 arbitrary: vs2)
+   apply(case_tac vs2)
+   apply(simp)    
+   apply(simp)
+   apply(case_tac vs2)
+   apply(simp)
+  apply(simp)
+done    
 
 lemma Posix_determ:
   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
@@ -1104,6 +1297,89 @@
   case (Posix_STAR2 r v2)
   have "[] \<in> STAR r \<rightarrow> v2" by fact
   then show "Stars [] = v2" by cases (auto simp add: Posix1)
+next
+  case (Posix_NTIMES2 vs r n v2)
+  then show "Stars vs = v2"
+    apply(erule_tac Posix_elims)
+     apply(auto)
+     apply (simp add: Posix1(2))
+    apply(rule List_eq_zipI)
+     apply(auto)
+    by (meson in_set_zipE)
+next
+  case (Posix_NTIMES1 s1 r v s2 n vs v2)
+  have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<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 (NTIMES r (n - 1 )))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+    using Posix1(1) apply fastforce
+    apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2)
+  using Posix1(2) by blast
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_UPNTIMES1 s1 r v s2 n vs v2)
+  have "(s1 @ s2) \<in> UPNTIMES r n \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (n - 1) \<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 (UPNTIMES r (n - 1 )))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r (n - 1)) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+    using Posix1(1) apply fastforce
+    apply (metis One_nat_def Posix1(1) Posix_UPNTIMES1.hyps(7) append.right_neutral append_self_conv2)
+  using Posix1(2) by blast
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> UPNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_UPNTIMES2 r n v2)
+  then show "Stars [] = v2"
+    apply(erule_tac Posix_elims)
+     apply(auto)
+    by (simp add: Posix1(2))
+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> []"
+       "\<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  
+  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+
+  ultimately show "Stars (v # vs) = v2" by auto    
+next
+  case (Posix_FROMNTIMES2 vs r n v2)  
+  then show "Stars vs = v2"
+    apply(erule_tac Posix_elims)
+     apply(auto)
+    apply(rule List_eq_zipI)
+     apply(auto)
+     apply(meson in_set_zipE)
+    by (simp add: Posix1(2))
+next
+  case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
+  then show "Stars (v # vs) = v2"
+    sorry
+next
+  case (Posix_NMTIMES2 vs r n m v2)
+  then show "Stars vs = v2"
+    sorry
 qed
 
 
@@ -1116,7 +1392,60 @@
   shows "v \<in> LV r s"
 using assms unfolding LV_def
 apply(induct rule: Posix.induct)
-apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
-done
-
+            apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[7]
+     defer
+  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(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
+    
+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