779 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
779 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
780 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; |
780 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; |
781 \<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))\<rbrakk> |
781 \<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))\<rbrakk> |
782 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
782 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
783 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
783 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
784 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
784 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
785 \<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))\<rbrakk> |
785 \<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))\<rbrakk> |
786 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
786 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
789 \<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> |
789 \<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> |
790 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
790 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
793 \<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> |
793 \<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> |
1162 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" |
1162 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" |
1163 "\<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))" by fact+ |
1163 "\<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))" by fact+ |
1164 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')" |
1164 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')" |
1165 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1165 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1166 using Posix1(1) apply fastforce |
1166 using Posix1(1) apply fastforce |
1167 by (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
1167 by (m etis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
1168 moreover |
1168 moreover |
1169 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1169 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1170 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1170 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1171 ultimately show "Stars (v # vs) = v2" by auto |
1171 ultimately show "Stars (v # vs) = v2" by auto |
1172 next |
1172 next |