619 apply (erule CollectE, (erule conjE|erule exE)+)

   619 apply (erule CollectE, (erule conjE|erule bexE)+)

   620 apply (simp split:if_splits)

   620 apply (simp add:proc_file_fds_def split:if_splits)

   621 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)

   621 apply (erule exE, rule_tac x = fda in exI)

   622 apply (case_tac "x = a", simp)

   622 apply (simp add:cfd2sfd_open2)

   623 apply (case_tac "x = a", simp add:proc_file_fds_def)

   624 apply (erule conjE|erule exE)+

   625 apply (erule conjE|erule bexE)+

   625 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)

   626 apply (rule_tac x = fda in bexI)

   626 apply (rule impI, drule proc_fd_in_fds, simp)

   627 apply (simp add:proc_file_fds_def, erule exE)

   627 apply (simp split:option.splits)

   628 apply (simp add:cfd2sfd_open2)

   629 apply (simp add:proc_file_fds_def)

   645 apply (erule CollectE, (erule exE|erule conjE)+)

   647 apply (simp add:proc_file_fds_def)

   648 apply (erule exE|erule conjE)+

   647 apply (rule CollectI)

   650 apply (rule_tac x = fda in exI, simp)

   648 apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp)

   651 apply (simp add:proc_file_fds_def)

   649 apply (erule CollectE, (erule exE|erule conjE)+)

   652 apply (erule exE|erule conjE)+

   650 apply (simp only:file_of_proc_fd.simps split:if_splits)

   651 apply (rule CollectI)

   668   "valid (Execve p fds # s) 

   669   "valid (Execve p f fds # s) 

   669    \<Longrightarrow> cpfd2sfds (Execve p fds # s)  = (cpfd2sfds s) (p := "

   670    \<Longrightarrow> cpfd2sfds (Execve p f fds # s) = (cpfd2sfds s) (p := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"

   671 apply (frule vd_cons, frule vt_grant_os)

   672 apply (rule ext)

   673 apply (rule set_eqI, rule iffI)

   674 unfolding cpfd2sfds_def proc_file_fds_def

   675 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   676 apply (simp split:if_splits)

   677 apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)

   678 apply (rule_tac x = fd in bexI, simp+)

   679 apply (simp add:cpfd2sfds_def proc_file_fds_def)

   680 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   681 apply (rule_tac x = fd in exI, simp)

   682 apply (simp split:if_splits)

   683 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   684 apply (rule_tac x = fd in exI, simp)

   685 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   686 apply (simp add:cpfd2sfds_def proc_file_fds_def)

   687 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   688 apply (rule_tac x = fd in exI, simp)

   689 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   690 done

   691 

   692 lemma cpfd2sfds_clone:

   693   "valid (Clone p p' fds shms # s) 

   694    \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"

   695 apply (frule vd_cons, frule vt_grant_os)

   696 apply (rule ext)

   697 apply (rule set_eqI, rule iffI)

   698 unfolding cpfd2sfds_def proc_file_fds_def

   699 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   700 apply (simp split:if_splits)

   701 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

   702 apply (rule_tac x = fd in bexI, simp+)

   703 apply (simp add:cpfd2sfds_def proc_file_fds_def)

   704 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

   705 apply (rule_tac x = fd in exI, simp)

   706 apply (simp split:if_splits)

   707 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   708 apply (rule_tac x = fd in exI, simp)

   709 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

   710 apply (simp add:cpfd2sfds_def proc_file_fds_def)

   711 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   712 apply (rule_tac x = fd in exI, simp)

   713 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

   714 done

   673     \<forall> 

   718     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   674 

   719     \<forall> p f fds. e \<noteq> Execve p f fds;

   675 lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other

   720     \<forall> p p'. e \<noteq> Kill p p';

   721     \<forall> p. e \<noteq> Exit p;

   722     \<forall> p fd. e \<noteq> CloseFd p fd;

   723     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"

   724 apply (frule vd_cons, frule vt_grant_os)

   725 apply (rule ext)

   726 unfolding cpfd2sfds_def proc_file_fds_def

   727 apply (case_tac e)

   728 using cfd2sfd_other

   729 by auto

   730 

   731 lemma cpfd2sfds_kill:

   732   "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"

   733 apply (frule vd_cons, frule vt_grant_os)

   734 apply (rule ext, rule set_eqI)

   735 unfolding cpfd2sfds_def proc_file_fds_def

   736 apply (rule iffI)

   737 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   738 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

   739 apply (rule_tac x = fd in exI, simp)

   740 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   741 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

   742 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   743 apply (rule_tac x = fd in exI, simp)

   744 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   745 done

   746 

   747 lemma cpfd2sfds_exit:

   748   "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"

   749 apply (frule vd_cons, frule vt_grant_os)

   750 apply (rule ext, rule set_eqI)

   751 unfolding cpfd2sfds_def proc_file_fds_def

   752 apply (rule iffI)

   753 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   754 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

   755 apply (rule_tac x = fd in exI, simp)

   756 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   757 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

   758 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   759 apply (rule_tac x = fd in exI, simp)

   760 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

   761 done

   762 

   763 lemma cpfd2sfds_closefd:

   764   "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := 

   765      if (fd \<in> proc_file_fds s p)

   766      then (case (cfd2sfd s p fd) of 

   767              Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)

   768                           then cpfd2sfds s p else cpfd2sfds s p - {sfd})

   769            | _        \<Rightarrow> cpfd2sfds s p)

   770      else cpfd2sfds s p)"

   771 apply (frule vd_cons)

   772 apply (rule ext, rule set_eqI, rule iffI)

   773 unfolding cpfd2sfds_def proc_file_fds_def

   774 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

   775 apply (simp split:if_splits)

   776 apply (rule conjI, rule impI, rule conjI, rule impI, erule exE)

   777 apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)

   778 apply (erule exE, simp)

   779 apply (rule conjI, rule impI, (erule exE|erule conjE)+)

   780 apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)

   781 

   782 apply (rule impI, rule conjI)

   783 apply (rule_tac x = fda in exI, simp, simp add:cfd2sfd_closefd)

   784 apply (rule notI, simp)

   785 apply (erule_tac x = fda in allE, simp add:cfd2sfd_closefd)

   786 

   787 apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)

   788 apply (erule exE, rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   789 

   790 apply (rule impI| rule conjI)+

   791 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   792 

   793 apply (rule impI, simp add:cpfd2sfds_def proc_file_fds_def)

   794 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   795 

   796 apply (simp split:if_splits)

   797 apply (frule_tac p = p and fd = fd in current_filefd_has_sfd, simp)

   798 apply (erule exE, simp)

   799 apply (case_tac "\<exists>fd'. fd' \<noteq> fd \<and> (\<exists>f'. file_of_proc_fd s p fd' = Some f') \<and> cfd2sfd s p fd' = Some sfd")

   800 apply simp

   801 apply (case_tac "xa = sfd")

   802 apply (erule exE|erule conjE)+

   803 apply (rule_tac x = fd' in exI, simp add:cfd2sfd_closefd)

   804 apply (erule exE|erule conjE)+

   805 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   806 apply (rule notI, simp)

   807 apply (simp, (erule exE|erule conjE)+)

   808 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   809 apply (rule notI, simp)

   810 apply (erule exE|erule conjE)+

   811 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   812 apply (rule notI, simp)

   813 apply (simp add:cpfd2sfds_def proc_file_fds_def)

   814 apply (erule exE|erule conjE)+

   815 apply (rule_tac x = fda in exI, simp add:cfd2sfd_closefd)

   816 done

   817 

   818 lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit

   819   cpfd2sfds_closefd cpfd2sfds_other

   820 

   821 (********* ch2sshm simpset ********)

   822 

   823 lemma ch2sshm_createshm:

   824   "valid (CreateShM p h # s) 

   825    \<Longrightarrow> ch2sshm (CreateShM p h # s) = (ch2sshm s) (h := 

   826      (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of

   827                     Some sec \<Rightarrow> 

   828  Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)

   829                   | _ \<Rightarrow> None))"

   830 apply (frule vd_cons, frule vt_grant_os)

   831 apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)

   832 done

   833 

   834 lemma ch2sshm_other:

   835   "\<lbrakk>valid (e # s); 

   836     \<forall> p h. e \<noteq> CreateShM p h; 

   837     h' \<in> current_shms (e # s)\<rbrakk> \<Longrightarrow> ch2sshm (e # s) h' = ch2sshm s h'"

   838 apply (frule vd_cons, frule vt_grant_os)

   839 apply (case_tac e)

   840 apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits)

   841 done

   842 

   843 lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other

   844 

   845 lemma current_shm_has_sh:

   846   "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sh. ch2sshm s h = Some sh"

   847 by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec')

   848 

   849 lemma current_shm_has_sh':

   850   "\<lbrakk>ch2sshm s h = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"

   851 by (auto dest:current_shm_has_sh)

   852 

   853 (********** cph2spshs simpset **********)

   854 

   855   (*???*) lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"

   856 apply (induct s arbitrary:p_flag)

   857 apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)

   858 apply (frule vd_cons, frule vt_grant_os)

   859 apply (case_tac a, auto split:if_splits option.splits)

   860 done

   861 

   862 definition

   863   "fff x z = {xx. \<exists> y. xx = (x,y) \<and> (x, y) \<in> z}"

   864 thm fff_def

   865 

   866 lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

   867 apply (induct s arbitrary:p flag)

   868 apply (simp, drule init_procs_has_shm, simp)

   869 apply (frule vd_cons, frule vt_grant_os)

   870 apply (case_tac a, auto split:if_splits option.splits)

   871 done

   872 

   873 

   874 lemma cph2spshs_createshm:

   875   "valid (Attach p h flag # s) \<Longrightarrow> 

   876    cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := 

   877      (case (ch2sshm s h) of 

   878         Some sh \<Rightarrow> cph2spshs s p \<union> {(sh, flag)}

   879       | _       \<Rightarrow> cph2spshs s p) )"

   880 apply (frule vd_cons, frule vt_grant_os, rule ext)

   881 unfolding cph2spshs_def

   882 using ch2sshm_other[where e = "Attach p h flag" and s = s]

   883 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits

   884 dest!:current_shm_has_sh'

   885 )

   886 thm current_shm_has_sshm

   887 apply (rule set_eqI, rule iffI)

   888 apply (case_tac xa, simp split:if_splits)

   889 apply (case_tac xa, erule CollectE)

   890 apply (simp, (erule conjE|erule bexE)+)

   891 apply (

   892 apply auto

   893 

   894 lemma cph2spshs_other:

   895   "\<lbrakk>valid (e # s); "

   896 

   897 lemmas cph2spshs_simps = cph2spshs_other