equal
deleted
inserted
replaced
715 shows "\<turnstile> v : r" |
715 shows "\<turnstile> v : r" |
716 using assms |
716 using assms |
717 apply(induct s r v rule: Posix.induct) |
717 apply(induct s r v rule: Posix.induct) |
718 apply(auto intro: Prf.intros) |
718 apply(auto intro: Prf.intros) |
719 using Prf.intros(8) Prf_UPNTIMES_bigger by blast |
719 using Prf.intros(8) Prf_UPNTIMES_bigger by blast |
|
720 |
|
721 lemma Posix_NTIMES_length: |
|
722 assumes "s \<in> NTIMES r n \<rightarrow> Stars vs" |
|
723 shows "length vs = n" |
|
724 using assms |
|
725 using NTIMES_Stars Posix1a val.inject(5) by blast |
|
726 |
|
727 lemma Posix_UPNTIMES_length: |
|
728 assumes "s \<in> UPNTIMES r n \<rightarrow> Stars vs" |
|
729 shows "length vs \<le> n" |
|
730 using assms |
|
731 using Posix1a UPNTIMES_Stars val.inject(5) by blast |
|
732 |
720 |
733 |
721 lemma Posix_NTIMES_mkeps: |
734 lemma Posix_NTIMES_mkeps: |
722 assumes "[] \<in> r \<rightarrow> mkeps r" |
735 assumes "[] \<in> r \<rightarrow> mkeps r" |
723 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
736 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
724 apply(induct n) |
737 apply(induct n) |