601 |
601 |
602 lemma current_filefd_has_sfd': |
602 lemma current_filefd_has_sfd': |
603 "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None" |
603 "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None" |
604 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd) |
604 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd) |
605 |
605 |
606 definition cpfd2sfds' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
606 lemma cpfd2sfds_open1: |
607 where |
607 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
608 "cpfd2sfds' s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}" |
608 cpfd2sfds (Open p f flags fd opt # s) p = ( |
609 |
609 case (cfd2sfd (Open p f flags fd opt # s) p fd) of |
610 definition cph2spshs' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
|
611 where |
|
612 "cph2spshs' s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
|
613 |
|
614 lemma "x \<in> cph2spshs' s p \<Longrightarrow> False" |
|
615 apply (simp add:cph2spshs'_def) |
|
616 apply (case_tac x, simp) |
|
617 |
|
618 |
|
619 lemma cpfd2sfds_open_some1: |
|
620 "valid (Open p f flags fd (Some inum) # s) \<Longrightarrow> |
|
621 cpfd2sfds (Open p f flags fd (Some inum) # s) p = ( |
|
622 case (cfd2sfd (Open p f flags fd (Some inum) # s) p fd) of |
|
623 Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd} |
610 Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd} |
624 | _ \<Rightarrow> cpfd2sfds s p)" |
611 | _ \<Rightarrow> cpfd2sfds s p)" |
625 apply (frule vd_cons, frule vt_grant_os) |
612 apply (frule vd_cons, frule vt_grant_os) |
626 apply (split option.splits) |
613 apply (split option.splits) |
627 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp) |
614 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp) |
628 apply (rule allI, rule impI) |
615 apply (rule allI, rule impI) |
629 apply (rule set_eqI, rule iffI) |
616 apply (rule set_eqI, rule iffI) |
|
617 apply (case_tac "x = a", simp) |
630 unfolding cpfd2sfds_def |
618 unfolding cpfd2sfds_def |
631 thm CollectE |
|
632 apply (erule CollectE) |
|
633 apply (erule CollectE, (erule conjE|erule exE)+) |
619 apply (erule CollectE, (erule conjE|erule exE)+) |
634 apply (simp only:file_of_proc_fd.simps split:if_splits) |
620 apply (simp split:if_splits) |
635 apply (simp add:cpfd2sfds_def) |
621 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) |
636 |
622 apply (case_tac "x = a", simp) |
637 apply (auto simp:cpfd2sfds_def split:option.splits if_splits dest:file_of_proc_fd_in_curf proc_fd_in_fds proc_fd_in_procs) |
623 apply (rule_tac x = fd in exI, simp+) |
638 |
624 apply (erule conjE|erule exE)+ |
639 lemma cpfd2sfds_open1: |
625 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) |
|
626 apply (rule impI, drule proc_fd_in_fds, simp) |
|
627 apply (simp split:option.splits) |
|
628 done |
|
629 |
|
630 lemma cpfd2sfds_open1': |
640 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
631 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
641 cpfd2sfds (Open p f flags fd opt # s) p = ( |
632 cpfd2sfds (Open p f flags fd opt # s) p = ( |
642 case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of |
633 case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of |
643 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
634 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
644 | _ \<Rightarrow> cpfd2sfds s p)" |
635 | _ \<Rightarrow> cpfd2sfds s p)" |
645 apply (frule vd_cons, frule vt_grant_os) |
|
646 apply (case_tac opt) |
|
647 apply (auto simp:sectxt_of_obj_simps current_files_simps dest!:current_has_sec' current_file_has_sfile' |
|
648 split:option.splits) |
|
649 apply (auto simp:cpfd2sfds_def split:if_splits) |
|
650 apply (auto simp:cfd2sfd_open cf2sfile_open sectxt_of_obj_simps current_files_simps split:option.splits if_splits dest!:current_has_sec' current_file_has_sfile') |
|
651 apply (frule cfd2sfd_open1) |
636 apply (frule cfd2sfd_open1) |
652 apply ( |
637 apply (auto dest:cpfd2sfds_open1 split:option.splits) |
653 apply (simp add:cpfd2sfds_def) |
638 done |
654 apply (auto simp add:cpfd2sfds_def split:option.splits) |
639 |
655 apply (auto dest!:current_has_sec') |
640 lemma cpfd2sfds_open2: |
|
641 "\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'" |
|
642 apply (frule vt_grant_os, frule vd_cons) |
|
643 unfolding cpfd2sfds_def |
|
644 apply (rule set_eqI, rule iffI) |
|
645 apply (erule CollectE, (erule exE|erule conjE)+) |
|
646 apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits) |
|
647 apply (rule CollectI) |
|
648 apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp) |
|
649 apply (erule CollectE, (erule exE|erule conjE)+) |
|
650 apply (simp only:file_of_proc_fd.simps split:if_splits) |
|
651 apply (rule CollectI) |
|
652 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) |
|
653 done |
656 |
654 |
657 lemma cpfd2sfds_open: |
655 lemma cpfd2sfds_open: |
658 "valid (Open p f flags fd opt # s) |
656 "valid (Open p f flags fd opt # s) |
659 \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := ( |
657 \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := ( |
660 case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of |
658 case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of |
661 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
659 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
662 | _ \<Rightarrow> cpfd2sfds s p))" |
660 | _ \<Rightarrow> cpfd2sfds s p))" |
663 apply (frule cfd2sfd_open1) |
|
664 apply (rule ext) |
661 apply (rule ext) |
665 apply (simp add:cpfd2sfds_def) |
662 apply (case_tac "x \<noteq> p") |
666 apply (auto simp add:cpfd2sfds_def split:option.splits) |
663 apply (simp add:cpfd2sfds_open2) |
667 |
664 apply (simp add:cpfd2sfds_open1') |
668 lemma cpfd2sfds_simps = |
665 done |
|
666 |
|
667 lemma cpfd2sfds_execve: |
|
668 "valid (Execve p fds # s) |
|
669 \<Longrightarrow> cpfd2sfds (Execve p fds # s) = (cpfd2sfds s) (p := " |
|
670 |
|
671 lemma cpfd2sfds_other: |
|
672 "\<lbrakk>valid (e # s); |
|
673 \<forall> |
|
674 |
|
675 lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other |
669 |
676 |
670 (******** cp2sproc simpset *********) |
677 (******** cp2sproc simpset *********) |
671 |
678 |
672 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p" |
679 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p" |
673 apply (simp add:cp2sproc_def) |
680 apply (simp add:cp2sproc_def) |