963 

   963 lemma cph2spshs_deleteshm:

   964   "valid (DeleteShM p h # s) \<Longrightarrow>     

   965    cph2spshs (DeleteShM p h # s) = (\<lambda> p'. 

   966     (case (ch2sshm s h, flag_of_proc_shm s p' h) of 

   967        (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)

   968                   then cph2spshs s p' else cph2spshs s p' - {(sh, flag)}

   969      | _       \<Rightarrow> cph2spshs s p')   )"

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

   971 

   972 apply (clarsimp)

   973 apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits)

   974 apply (rule conjI, rule impI)

   975 using ch2sshm_other[where e = "DeleteShM p h" and s = s] 

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

   977 dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1]

   978 apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+)

   979 apply (rule_tac x = ha in exI, simp)

   980 apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+)

   981 

   982 apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+

   983 

   984 apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)

   985 apply (erule CollectE | erule exE| erule conjE| rule CollectI)+

   986 apply (case_tac "ha = h", simp)

   987 apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp)

   988 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

   989 

   990 apply (erule CollectE | erule exE| erule conjE| rule CollectI)+

   991 apply (case_tac "ha = h", simp)

   992 apply (rule_tac x = h' in exI, simp)

   993 apply (frule_tac flag = flag in procs_of_shm_prop4, simp+)

   994 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

   995 apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp)

   996 apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)

   997 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

   998 

   999 apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+

  1000 apply (simp only:cph2spshs_def, rule set_eqI, rule iffI)

  1001 apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+

  1002 apply (simp split:if_splits)

  1003 apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)

  1004 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

  1005 apply (rule notI, simp split:if_splits)

  1006 apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+)

  1007 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

  1008 apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+

  1009 apply (simp split:if_splits)

  1010 apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp)

  1011 apply (case_tac "ha = h", simp add:procs_of_shm_prop4)

  1012 apply (frule_tac h = ha in procs_of_shm_prop1, simp+)

  1013 using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1)

  1014 done

  1015 

  1016 lemma flag_of_proc_shm_prop1:

  1017   "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"

  1018 apply (induct s arbitrary:p)

  1019 apply (simp add:init_shmflag_has_proc)

  1020 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits)

  1021 done

  1022 

  1023 lemma cph2spshs_clone:

  1024   "valid (Clone p p' fds shms # s) \<Longrightarrow> 

  1025    cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' := 

  1026      {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag} )"

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

  1028 using ch2sshm_other[where e = "Clone p p' fds shms" and s = s]

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

  1030 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)

  1031 apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4)

  1032 apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1)

  1033 apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)+

  1034 done

  1035 

  1036 lemma cph2spshs_execve:

  1037   "valid (Execve p f fds # s) \<Longrightarrow>

  1038   cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})"

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

  1040 using ch2sshm_other[where e = "Execve p f fds" and s = s]

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

  1042 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)

  1043 apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+

  1044 done

  1045 

  1046 lemma cph2spshs_kill:

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

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

  1049 using ch2sshm_other[where e = "Kill p p'" and s = s]

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

  1051 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)

  1052 apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+

  1053 done

  1054 

  1055 lemma cph2spshs_exit:

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

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

  1058 using ch2sshm_other[where e = "Exit p" and s = s]

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

  1060 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)

  1061 apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+

  1062 done

  1063 

  1064 lemma cph2spshs_createshm:

  1065   "valid (CreateShM p h # s) \<Longrightarrow> cph2spshs (CreateShM p h # s) = cph2spshs s"

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

  1067 apply (auto simp:cph2spshs_def)

  1068 using ch2sshm_createshm

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

  1070 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def)

  1071 apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1)

  1072 done

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

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

   967 

  1076     \<forall> p h flag. e \<noteq> Attach p h flag;

   968 lemmas cph2spshs_simps = cph2spshs_other

  1077     \<forall> p h. e \<noteq> Detach p h;

  1078     \<forall> p h. e \<noteq> DeleteShM p h;

  1079     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

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

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

  1082     \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cph2spshs (e # s) = cph2spshs s"

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

  1084 unfolding cph2spshs_def 

  1085 apply (rule set_eqI, rule iffI)

  1086 apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)+

  1087 apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI)

  1088 apply (case_tac e)

  1089 using ch2sshm_other[where e = e and s = s] 

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

  1091 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3

  1092  simp:ch2sshm_createshm)

  1093 apply (rule_tac x = h in exI, case_tac e)

  1094 using ch2sshm_other[where e = e and s = s] 

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

  1096 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 

  1097  simp:ch2sshm_createshm)

  1098 done

  1099 

  1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve

  1101   cph2spshs_exit cph2spshs_kill cph2spshs_other