equal
deleted
inserted
replaced
1157 apply(auto) |
1157 apply(auto) |
1158 done |
1158 done |
1159 next |
1159 next |
1160 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1160 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
1161 have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" |
1161 have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" |
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" "flat v = [] \<Longrightarrow> flat (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 (m etis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2) |
1167 by (metis Posix1(1) Posix_NMTIMES1.hyps(6) self_append_conv self_append_conv2) |
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 |
1567 apply(rule Posix.intros) |
1567 apply(rule Posix.intros) |
1568 apply(rule IH) |
1568 apply(rule IH) |
1569 apply(blast) |
1569 apply(blast) |
1570 apply(simp) |
1570 apply(simp) |
1571 apply(simp add: der_correctness Der_def) |
1571 apply(simp add: der_correctness Der_def) |
|
1572 using Posix1a Prf_injval_flat list.distinct(1) apply auto[1] |
|
1573 apply(simp add: der_correctness Der_def) |
1572 done |
1574 done |
1573 next |
1575 next |
1574 case (PLUS r) |
1576 case (PLUS r) |
1575 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1577 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1576 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |
1578 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |