188 apply(subst append.simps(1)[symmetric]) |
187 apply(subst append.simps(1)[symmetric]) |
189 apply(rule Posix.intros) |
188 apply(rule Posix.intros) |
190 apply(auto) |
189 apply(auto) |
191 done |
190 done |
192 |
191 |
193 lemma test: |
|
194 assumes "s \<in> der c (FROMNTIMES r 0) \<rightarrow> v" |
|
195 shows "XXX" |
|
196 using assms |
|
197 apply(simp) |
|
198 apply(erule Posix_elims) |
|
199 apply(drule FROMNTIMES_0) |
|
200 apply(auto) |
|
201 oops |
|
202 |
192 |
203 lemma Posix_injval: |
193 lemma Posix_injval: |
204 assumes "s \<in> (der c r) \<rightarrow> v" |
194 assumes "s \<in> (der c r) \<rightarrow> v" |
205 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
195 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
206 using assms |
196 using assms |
452 then consider |
442 then consider |
453 (cons) v1 vs s1 s2 where |
443 (cons) v1 vs s1 s2 where |
454 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
444 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
455 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
445 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
456 "\<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 (FROMNTIMES r (n - 1)))" |
446 "\<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 (FROMNTIMES r (n - 1)))" |
457 | (null) v1 where |
447 | (null) v1 vs s1 s2 where |
458 "v = Seq v1 (Stars [])" |
448 "v = Seq v1 (Stars vs)" "s = s1 @ s2" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
459 "s \<in> der c r \<rightarrow> v1" "[] \<in> (FROMNTIMES r 0) \<rightarrow> (Stars [])" "n = 0" |
449 "s1 \<in> der c r \<rightarrow> v1" "n = 0" |
|
450 "\<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 (STAR r))" |
460 (* here *) |
451 (* here *) |
461 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
452 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
462 apply(erule Posix_elims) |
453 prefer 2 |
463 apply(simp) |
454 apply(erule Posix_elims) |
464 apply(case_tac "n = 0") |
455 apply(simp) |
465 apply(simp) |
|
466 apply(drule FROMNTIMES_0) |
|
467 apply(simp) |
|
468 using FROMNTIMES_0 Posix_mkeps apply force |
|
469 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
456 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
470 apply(clarify) |
457 apply(clarify) |
471 apply(drule_tac x="v1" in meta_spec) |
458 apply(drule_tac x="v1" in meta_spec) |
472 apply(drule_tac x="vss" in meta_spec) |
459 apply(drule_tac x="vss" in meta_spec) |
473 apply(drule_tac x="s1" in meta_spec) |
460 apply(drule_tac x="s1" in meta_spec) |
474 apply(drule_tac x="s2" in meta_spec) |
461 apply(drule_tac x="s2" in meta_spec) |
475 apply(simp add: der_correctness Der_def) |
462 apply(simp add: der_correctness Der_def) |
476 apply(case_tac "n = 0") |
463 apply(rotate_tac 5) |
|
464 apply(erule Posix_elims) |
|
465 apply(auto)[2] |
|
466 apply(erule Posix_elims) |
477 apply(simp) |
467 apply(simp) |
478 apply(simp) |
468 apply blast |
479 apply(rotate_tac 4) |
469 apply(erule Posix_elims) |
|
470 apply(auto) |
|
471 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
|
472 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
|
473 apply(clarify) |
|
474 apply simp |
|
475 apply(rotate_tac 6) |
480 apply(erule Posix_elims) |
476 apply(erule Posix_elims) |
481 apply(auto)[2] |
477 apply(auto)[2] |
482 done |
478 done |
483 then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v" |
479 then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v" |
484 proof (cases) |
480 proof (cases) |
485 case cons |
481 case cons |
486 have "s1 \<in> der c r \<rightarrow> v1" by fact |
482 have "s1 \<in> der c r \<rightarrow> v1" by fact |
487 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
483 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
506 apply(simp) |
502 apply(simp) |
507 done |
503 done |
508 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
504 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
509 next |
505 next |
510 case null |
506 case null |
511 have "s \<in> der c r \<rightarrow> v1" by fact |
507 have "s1 \<in> der c r \<rightarrow> v1" by fact |
512 then have "(c # s) \<in> r \<rightarrow> injval r c v1" using IH by simp |
508 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
513 moreover |
509 moreover |
514 have "[] \<in> (FROMNTIMES r 0) \<rightarrow> Stars []" by fact |
510 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact |
515 moreover |
511 moreover |
516 have "(c # s) \<in> r \<rightarrow> injval r c v1" by fact |
512 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
517 then have "flat (injval r c v1) = (c # s)" by (rule Posix1) |
513 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
518 then have "flat (injval r c v1) \<noteq> []" by simp |
514 then have "flat (injval r c v1) \<noteq> []" by simp |
|
515 moreover |
|
516 moreover |
|
517 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 (STAR r))" by fact |
|
518 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 (STAR r))" |
|
519 by (simp add: der_correctness Der_def) |
519 ultimately |
520 ultimately |
520 have "((c # s) @ []) \<in> FROMNTIMES r 1 \<rightarrow> Stars [injval r c v1]" |
521 have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" |
521 apply (rule_tac Posix.intros) |
522 apply (rule_tac Posix.intros) back |
522 apply(simp_all) |
523 apply(simp_all) |
523 done |
524 done |
524 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null |
525 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null |
525 apply(simp) |
526 apply(simp) |
526 apply(erule Posix_elims) |
527 done |
527 apply(auto) |
|
528 apply(rotate_tac 6) |
|
529 apply(drule FROMNTIMES_0) |
|
530 apply(simp) |
|
531 sorry |
|
532 qed |
528 qed |
533 next |
529 next |
534 case (NMTIMES x1 x2 m s v) |
530 case (NMTIMES x1 x2 m s v) |
535 then show ?case sorry |
531 then show ?case sorry |
536 qed |
532 qed |