435 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
435 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
436 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
436 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
437 \<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> |
437 \<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> |
438 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
438 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
439 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
439 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
440 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
440 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
441 \<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 - 1)))\<rbrakk> |
441 \<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> |
442 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)" |
442 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (n + 1) \<rightarrow> Stars (v # vs)" |
443 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
443 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
444 \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs" |
444 \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs" |
445 |
445 |
446 inductive_cases Posix_elims: |
446 inductive_cases Posix_elims: |
447 "s \<in> ZERO \<rightarrow> v" |
447 "s \<in> ZERO \<rightarrow> v" |
456 assumes "s \<in> r \<rightarrow> v" |
456 assumes "s \<in> r \<rightarrow> v" |
457 shows "s \<in> L r" "flat v = s" |
457 shows "s \<in> L r" "flat v = s" |
458 using assms |
458 using assms |
459 apply(induct s r v rule: Posix.induct) |
459 apply(induct s r v rule: Posix.induct) |
460 apply(auto simp add: pow_empty_iff) |
460 apply(auto simp add: pow_empty_iff) |
461 apply (metis Suc_pred concI lang_pow.simps(2)) |
|
462 by (meson ex_in_conv set_empty) |
461 by (meson ex_in_conv set_empty) |
463 |
462 |
464 lemma Posix1a: |
463 lemma Posix1a: |
465 assumes "s \<in> r \<rightarrow> v" |
464 assumes "s \<in> r \<rightarrow> v" |
466 shows "\<Turnstile> v : r" |
465 shows "\<Turnstile> v : r" |
564 apply(rule List_eq_zipI) |
563 apply(rule List_eq_zipI) |
565 apply(auto simp add: list_all2_iff) |
564 apply(auto simp add: list_all2_iff) |
566 by (meson in_set_zipE) |
565 by (meson in_set_zipE) |
567 next |
566 next |
568 case (Posix_NTIMES1 s1 r v s2 n vs) |
567 case (Posix_NTIMES1 s1 r v s2 n vs) |
569 have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" |
568 have "(s1 @ s2) \<in> NTIMES r (n + 1) \<rightarrow> v2" |
570 "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
569 "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r n \<rightarrow> Stars vs" "flat v \<noteq> []" |
571 "\<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 - 1 )))" by fact+ |
570 "\<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))" by fact+ |
572 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
571 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')" |
573 apply(cases) apply (auto simp add: append_eq_append_conv2) |
572 apply(cases) apply (auto simp add: append_eq_append_conv2) |
574 using Posix1(1) apply fastforce |
573 using Posix1(1) apply fastforce |
575 apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2) |
574 apply (metis L.simps(7) Posix1(1) append.left_neutral append.right_neutral) |
576 using Posix1(2) by blast |
575 using Posix1(2) by blast |
577 moreover |
576 moreover |
578 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
577 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
579 "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
578 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
580 ultimately show "Stars (v # vs) = v2" by auto |
579 ultimately show "Stars (v # vs) = v2" by auto |
581 qed |
580 qed |
582 |
581 |
583 |
582 |
584 text \<open> |
583 text \<open> |
588 lemma Posix_LV: |
587 lemma Posix_LV: |
589 assumes "s \<in> r \<rightarrow> v" |
588 assumes "s \<in> r \<rightarrow> v" |
590 shows "v \<in> LV r s" |
589 shows "v \<in> LV r s" |
591 using assms unfolding LV_def |
590 using assms unfolding LV_def |
592 apply(induct rule: Posix.induct) |
591 apply(induct rule: Posix.induct) |
593 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a) |
592 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a) |
594 apply (smt (verit, best) One_nat_def Posix1a Posix_NTIMES1 L.simps(7)) |
593 apply (smt (verit, ccfv_SIG) L.simps(7) Posix1a Posix_NTIMES1 Suc_eq_plus1) |
595 using Posix1a Posix_NTIMES2 by blast |
594 using Posix1a Posix_NTIMES2 by blast |
596 |
595 |
597 |
596 |
598 end |
597 end |