669 using PosOrd_spreI as1(1) eqs by blast |
669 using PosOrd_spreI as1(1) eqs by blast |
670 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
670 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
671 by (auto simp add: LV_def) |
671 by (auto simp add: LV_def) |
672 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
672 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
673 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
673 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
|
674 thm PosOrd_SeqI1 PosOrd_SeqI2 |
674 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
675 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) |
675 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
676 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
676 next |
677 next |
677 case (Posix_STAR1 s1 r v s2 vs v3) |
678 case (Posix_STAR1 s1 r v s2 vs v3) |
678 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
679 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
688 "flat (Stars (v3a # vs3)) = s1 @ s2" |
689 "flat (Stars (v3a # vs3)) = s1 @ s2" |
689 | (Empty) "v3 = Stars []" |
690 | (Empty) "v3 = Stars []" |
690 unfolding LV_def |
691 unfolding LV_def |
691 apply(auto) |
692 apply(auto) |
692 apply(erule Prf.cases) |
693 apply(erule Prf.cases) |
693 apply(simp_all) |
694 apply(auto) |
694 apply(auto)[1] |
|
695 apply(case_tac vs) |
695 apply(case_tac vs) |
696 apply(auto) |
696 apply(auto intro: Prf.intros) |
697 using Prf.intros(6) by blast |
697 done |
698 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
698 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
699 proof (cases) |
699 proof (cases) |
700 case (NonEmpty v3a vs3) |
700 case (NonEmpty v3a vs3) |
701 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
701 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
702 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
702 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
819 then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def |
819 then show "s \<in> ZERO \<rightarrow> v1" unfolding LV_def |
820 by (auto elim: Prf.cases) |
820 by (auto elim: Prf.cases) |
821 next |
821 next |
822 case (ONE s v1) |
822 case (ONE s v1) |
823 have "v1 \<in> LV ONE s" by fact |
823 have "v1 \<in> LV ONE s" by fact |
824 then show "s \<in> ONE \<rightarrow> v1" unfolding LV_def |
824 then have "v1 = Void" "s = []" unfolding LV_def |
825 by(auto elim!: Prf.cases intro: Posix.intros) |
825 by(auto elim: Prf.cases) |
|
826 then show "s \<in> ONE \<rightarrow> v1" |
|
827 by(auto intro: Posix.intros) |
826 next |
828 next |
827 case (CHAR c s v1) |
829 case (CHAR c s v1) |
828 have "v1 \<in> LV (CHAR c) s" by fact |
830 have "v1 \<in> LV (CHAR c) s" by fact |
829 then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def |
831 then show "s \<in> CHAR c \<rightarrow> v1" unfolding LV_def |
830 by (auto elim!: Prf.cases intro: Posix.intros) |
832 by (auto elim!: Prf.cases intro: Posix.intros) |
831 next |
833 next |
832 case (ALT r1 r2 s v1) |
834 case (ALT r1 r2 s v1) |
833 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
835 have IH1: "\<And>s v1. \<lbrakk>v1 \<in> LV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact |
834 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
836 have IH2: "\<And>s v1. \<lbrakk>v1 \<in> LV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact |
835 have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
837 have as1: "\<forall>v2 \<in> LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact |
836 have as2: "v1 \<in> LV (ALT r1 r2) s" by fact |
838 have as2: "v1 \<in> LV (ALT r1 r2) s" by fact |
837 then consider |
839 then consider |
838 (Left) v1' where |
840 (Left) v1' where |
839 "v1 = Left v1'" "s = flat v1'" |
841 "v1 = Left v1'" "s = flat v1'" |
840 "v1' \<in> LV r1 s" |
842 "v1' \<in> LV r1 s" |
843 "v1' \<in> LV r2 s" |
845 "v1' \<in> LV r2 s" |
844 unfolding LV_def by (auto elim: Prf.cases) |
846 unfolding LV_def by (auto elim: Prf.cases) |
845 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
847 then show "s \<in> ALT r1 r2 \<rightarrow> v1" |
846 proof (cases) |
848 proof (cases) |
847 case (Left v1') |
849 case (Left v1') |
848 have "v1' \<in> LV r1 s" using as2 |
850 have "v1' \<in> LV r1 s" using Left(3) . |
849 unfolding LV_def Left by (auto elim: Prf.cases) |
|
850 moreover |
851 moreover |
851 have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
852 have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
852 unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force |
853 unfolding Left(1,2) unfolding LV_def |
|
854 using Prf.intros(2) PosOrd_Left_eq by force |
853 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
855 ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp |
854 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
856 then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros) |
855 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
857 then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp |
856 next |
858 next |
857 case (Right v1') |
859 case (Right v1') |
858 have "v1' \<in> LV r2 s" using as2 |
860 have "v1' \<in> LV r2 s" using Right(3) . |
859 unfolding LV_def Right by (auto elim: Prf.cases) |
|
860 moreover |
861 moreover |
861 have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
862 have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1 |
862 unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
863 unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force |
863 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
864 ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp |
864 moreover |
865 moreover |