equal
deleted
inserted
replaced
256 then consider |
256 then consider |
257 (cons) v1 vs s1 s2 where |
257 (cons) v1 vs s1 s2 where |
258 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
258 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
259 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
259 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
260 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
260 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
261 |
|
262 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
261 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
263 apply(erule Posix_elims) |
262 apply(erule Posix_elims) |
264 apply(simp) |
263 apply(simp) |
265 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
264 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
266 apply(clarify) |
265 apply(clarify) |
285 moreover |
284 moreover |
286 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact |
285 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact |
287 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
286 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
288 by (simp add: der_correctness Der_def) |
287 by (simp add: der_correctness Der_def) |
289 ultimately |
288 ultimately |
290 have "((c # s1) @ s2) \<in> NTIMES r n \<rightarrow> Stars (injval r c v1 # vs)" |
289 have "((c # s1) @ s2) \<in> NTIMES r n \<rightarrow> Stars (injval r c v1 # vs)" |
291 apply (rule_tac Posix.intros) |
290 by (metis One_nat_def Posix_NTIMES1 Suc_eq_plus1 Suc_pred cons(5)) |
292 apply(simp_all) |
|
293 apply(case_tac n) |
|
294 apply(simp) |
|
295 using Posix_elims(1) NTIMES.prems apply auto[1] |
|
296 apply(simp) |
|
297 done |
|
298 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
291 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
299 qed |
292 qed |
300 |
293 |
301 qed |
294 qed |
302 |
295 |