--- a/thys/SpecExt.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/SpecExt.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -505,7 +505,10 @@
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];
     length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"
 
-  
+
+ 
+
+
 inductive_cases Prf_elims:
   "\<Turnstile> v : ZERO"
   "\<Turnstile> v : SEQ r1 r2"
@@ -764,7 +767,34 @@
   shows "L(r) = {flat v | v. \<Turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
+thm Prf.intros
+thm Prf.cases
 
+lemma
+  assumes "\<Turnstile> v : (STAR r)" 
+  shows "\<Turnstile> v : (FROMNTIMES r 0)"
+  using assms
+  apply(erule_tac Prf.cases)
+             apply(simp_all)
+  apply(case_tac vs)
+   apply(auto)
+  apply(subst append_Nil[symmetric])
+   apply(rule Prf.intros)
+     apply(auto)
+  apply(simp add: Prf.intros)
+  done
+
+lemma
+  assumes "\<Turnstile> v : (FROMNTIMES r 0)" 
+  shows "\<Turnstile> v : (STAR r)"
+  using assms
+  apply(erule_tac Prf.cases)
+             apply(simp_all)
+   apply(rule Prf.intros)
+   apply(simp)
+  apply(rule Prf.intros)
+   apply(simp)
+  done
 
 section {* Sets of Lexical Values *}