866 apply (case_tac a, auto split:if_splits option.splits) |
866 apply (case_tac a, auto split:if_splits option.splits) |
867 done |
867 done |
868 |
868 |
869 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk> |
869 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk> |
870 \<Longrightarrow> flag = flag'" |
870 \<Longrightarrow> flag = flag'" |
871 apply (induct s arbitrary:p) |
871 apply (induct s arbitrary:p flag flag') |
872 apply (simp) |
872 apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp) |
873 apply( drule init_procs_has_shm, simp) |
873 apply (frule vd_cons, frule vt_grant_os) |
874 apply (frule vd_cons, frule vt_grant_os) |
874 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) |
875 apply (case_tac a, auto split:if_splits option.splits) |
875 done |
876 done |
876 |
877 |
877 lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag" |
|
878 apply (induct s arbitrary:p flag) |
|
879 apply (simp, drule init_procs_has_shm, simp) |
|
880 apply (frule vd_cons, frule vt_grant_os) |
|
881 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) |
|
882 done |
|
883 |
|
884 lemma procs_of_shm_prop4': |
|
885 "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h" |
|
886 by (auto dest:procs_of_shm_prop4) |
878 |
887 |
879 lemma cph2spshs_attach: |
888 lemma cph2spshs_attach: |
880 "valid (Attach p h flag # s) \<Longrightarrow> |
889 "valid (Attach p h flag # s) \<Longrightarrow> |
881 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
890 cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := |
882 (case (ch2sshm s h) of |
891 (case (ch2sshm s h) of |
899 apply (rule impI, simp) |
908 apply (rule impI, simp) |
900 done |
909 done |
901 |
910 |
902 lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow> |
911 lemma cph2spshs_detach: "valid (Detach p h # s) \<Longrightarrow> |
903 cph2spshs (Detach p h # s) = (cph2spshs s) (p := |
912 cph2spshs (Detach p h # s) = (cph2spshs s) (p := |
904 (case (ch2sshm s h) of |
913 (case (ch2sshm s h, flag_of_proc_shm s p h) of |
905 Some sh \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> p \<in> procs_of_shm s h' \<and> ch2sshm s p h' = Some sh) |
914 (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) |
906 then cph2spshs s p else cph2spshs s p - {(sh, flag) | flag. (sh, flag) \<in> cph2spshs s p} |
915 then cph2spshs s p else cph2spshs s p - {(sh, flag)} |
907 | _ \<Rightarrow> cph2spshs s p) )" |
916 | _ \<Rightarrow> cph2spshs s p) )" |
908 apply (frule vd_cons, frule vt_grant_os, rule ext) |
917 apply (frule vd_cons, frule vt_grant_os, rule ext) |
909 using ch2sshm_other[where e = "Detach p h" and s = s] |
918 apply (case_tac "x = p") defer |
|
919 using ch2sshm_other[where e = "Detach p h" and s = s] |
910 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits |
920 apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits |
911 dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def) |
921 dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1] |
912 apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) |
922 apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) |
913 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
923 apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) |
914 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
915 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
916 apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) |
|
917 apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp) |
|
918 apply (rule_tac x = ha in exI, simp) |
|
919 apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp) |
|
920 apply (rule_tac x = ha in exI, simp) |
|
921 apply (frule procs_of_shm_prop1, simp, simp) |
|
922 apply (rule impI, simp) |
924 apply (rule impI, simp) |
923 done |
925 |
|
926 apply (clarsimp) |
|
927 apply (frule current_shm_has_sh, simp, erule exE) |
|
928 apply (frule procs_of_shm_prop4, simp, simp) |
|
929 apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ |
|
930 |
|
931 apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) |
|
932 apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ |
|
933 apply (case_tac "ha = h", simp) |
|
934 apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp) |
|
935 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
936 |
|
937 apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ |
|
938 apply (case_tac "ha = h", simp) |
|
939 apply (rule_tac x = h' in exI, simp) |
|
940 apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+) |
|
941 apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+) |
|
942 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
943 apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp) |
|
944 apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) |
|
945 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
946 |
|
947 apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ |
|
948 apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) |
|
949 apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+ |
|
950 apply (simp split:if_splits) |
|
951 apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) |
|
952 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
953 apply (rule notI, simp split:if_splits) |
|
954 apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) |
|
955 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
956 apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+ |
|
957 apply (simp split:if_splits) |
|
958 apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp) |
|
959 apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+) |
|
960 using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) |
|
961 done |
|
962 |
|
963 |
924 |
964 |
925 lemma cph2spshs_other: |
965 lemma cph2spshs_other: |
926 "\<lbrakk>valid (e # s); " |
966 "\<lbrakk>valid (e # s); " |
927 |
967 |
928 lemmas cph2spshs_simps = cph2spshs_other |
968 lemmas cph2spshs_simps = cph2spshs_other |
979 apply (case_tac e) |
1002 apply (case_tac e) |
980 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
1003 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
981 |
1004 |
982 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
1005 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
983 |
1006 |
984 (********************** cfd2fd_s simpset ******************************) |
1007 |
985 |
|
986 lemma cfd2fd_s_nil: "fd \<in> init_fds_of_proc p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd" |
|
987 by (simp add:cfd2fd_s_def index_of_fd.simps) |
|
988 |
|
989 lemma cfd2fd_s_nil': "fd \<in> current_proc_fds [] p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd" |
|
990 by (simp add:cfd2fd_s_nil current_proc_fds.simps) |
|
991 |
|
992 lemma cfd2fd_s_open: "cfd2fd_s (Open p f flags fd opt # \<tau>) p' fd' = ( |
|
993 if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) |
|
994 else cfd2fd_s \<tau> p' fd') |
|
995 else cfd2fd_s \<tau> p' fd' )" |
|
996 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps) |
|
997 |
|
998 lemma cfd2fd_s_createsock: "cfd2fd_s (CreateSock p af st fd im # \<tau>) p' fd' = ( |
|
999 if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) |
|
1000 else cfd2fd_s \<tau> p' fd') |
|
1001 else cfd2fd_s \<tau> p' fd' )" |
|
1002 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps) |
|
1003 |
|
1004 lemma cfd2fd_s_accept: "cfd2fd_s (Accept p fd addr port fd' im # \<tau>) p' fd'' = ( |
|
1005 if (p' = p) then (if (fd'' = fd') then SCrea (Suc (length \<tau>)) |
|
1006 else cfd2fd_s \<tau> p' fd'') |
|
1007 else cfd2fd_s \<tau> p' fd'' )" |
|
1008 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps) |
|
1009 |
|
1010 lemma cfd2fd_s_clone: "cfd2fd_s (Clone p p' # \<tau>) p'' fd = (if (p'' = p') then cfd2fd_s \<tau> p fd else cfd2fd_s \<tau> p'' fd)" |
|
1011 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps) |
|
1012 |
|
1013 lemma cfd2fd_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
1014 \<forall> p af st fd im. e \<noteq> CreateSock p af st fd im; |
|
1015 \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im; |
|
1016 \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> cfd2fd_s (e # \<tau>) p'' fd'' = cfd2fd_s \<tau> p'' fd''" |
|
1017 by (case_tac e, auto simp:cfd2fd_s_def index_of_fd.simps d2s_aux.simps) |
|
1018 |
|
1019 lemmas cfd2fd_s_simps = cfd2fd_s_nil cfd2fd_s_nil' cfd2fd_s_open cfd2fd_s_createsock cfd2fd_s_accept cfd2fd_s_clone cfd2fd_s_other |
|
1020 |
|
1021 (************* cim2im_s simpset **************************) |
|
1022 |
|
1023 (* no such lemma |
|
1024 lemma cim2im_s_nil: "init_itag_of_inum im = Some tag \<Longrightarrow> cim2im_s [] im = SInit im" |
|
1025 by (simp add:cim2im_s_def) |
|
1026 *) |
|
1027 |
|
1028 lemma cim2im_s_open: "cim2im_s (Open p f flags fd (Some im) # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')" |
|
1029 by (simp add:cim2im_s_def) |
|
1030 |
|
1031 lemma cim2im_s_open': "cim2im_s (Open p f flags fd None # \<tau>) im = cim2im_s \<tau> im" |
|
1032 by (simp add:cim2im_s_def) |
|
1033 |
|
1034 lemma cim2im_s_mkdir: "cim2im_s (Mkdir p f im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')" |
|
1035 by (simp add:cim2im_s_def) |
|
1036 |
|
1037 lemma cim2im_s_createsock: "cim2im_s (CreateSock p sf st fd im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')" |
|
1038 by (simp add:cim2im_s_def) |
|
1039 |
|
1040 lemma cim2im_s_accept: "cim2im_s (Accept p fd addr port fd' im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')" |
|
1041 by (simp add:cim2im_s_def) |
|
1042 |
|
1043 lemma cim2im_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
1044 \<forall> p f im. e \<noteq> Mkdir p f im; |
|
1045 \<forall> p sf st fd im. e \<noteq> CreateSock p sf st fd im; |
|
1046 \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im\<rbrakk> \<Longrightarrow> cim2im_s (e # \<tau>) im = cim2im_s \<tau> im" |
|
1047 by (case_tac e, auto simp:cim2im_s_def) |
|
1048 |
|
1049 lemmas cim2im_s_simps = cim2im_s_open cim2im_s_open' cim2im_s_mkdir cim2im_s_createsock cim2im_s_accept cim2im_s_other |
|
1050 |
|
1051 |
|
1052 lemma cig2ig_s_simp: "cig2ig_s (e # \<tau>) tag = cig2ig_s \<tau> tag" |
|
1053 apply (case_tac tag) |
|
1054 by auto |
|
1055 |
|
1056 (******************* cobj2sobj no Suc (length \<tau>) ***********************) |
|
1057 |
|
1058 lemma cf2sfile_le_len: "\<lbrakk>cf2sfile \<tau> f = SCrea (Suc (length \<tau>)) # spf; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False" |
|
1059 apply (case_tac f, (simp add:cf2sfile.simps d2s_aux.simps)+) |
|
1060 apply (case_tac "index_of_file \<tau> (a # list)", (simp add:d2s_aux.simps)+) |
|
1061 by (drule index_of_file_le_length', simp+) |
|
1062 |
|
1063 lemma cf2sfile_le_len': "\<lbrakk>SCrea (Suc (length \<tau>)) # spf \<preceq> cf2sfile \<tau> f; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False" |
|
1064 apply (induct f) |
|
1065 apply (simp add:no_junior_def cf2sfile.simps d2s_aux.simps) |
|
1066 apply (case_tac "cf2sfile \<tau> (a # f) = SCrea (Suc (length \<tau>)) # spf") |
|
1067 apply (drule_tac f = "a # f" in cf2sfile_le_len, simp+) |
|
1068 apply (simp only:cf2sfile.simps d2s_aux.simps) |
|
1069 apply (drule_tac no_junior_noteq, simp+) |
|
1070 apply (rule impI, erule impE, simp+) |
|
1071 apply (drule parentf_in_current', simp+) |
|
1072 done |
|
1073 |
|
1074 lemma cp2sproc_le_len: "cp2sproc \<tau> p = SCrea (Suc (length \<tau>)) \<Longrightarrow> False" |
|
1075 apply (simp add:cp2sproc_def, case_tac "index_of_proc \<tau> p") |
|
1076 apply (simp add:d2s_aux.simps)+ |
|
1077 by (drule index_of_proc_le_length', simp) |
|
1078 |
|
1079 lemma ch2sshm_le_len: "ch2sshm \<tau> h = SCrea (Suc (length \<tau>)) \<Longrightarrow> False" |
|
1080 apply (simp add:ch2sshm_def, case_tac "index_of_shm \<tau> h") |
|
1081 apply (simp add:d2s_aux.simps)+ |
|
1082 by (drule index_of_shm_le_length', simp) |
|
1083 |
|
1084 lemma cm2smsg_le_len: "cm2smsg \<tau> m = SCrea (Suc (length \<tau>)) \<Longrightarrow> False" |
|
1085 apply (simp add:cm2smsg_def, case_tac "index_of_msg \<tau> m") |
|
1086 apply (simp add:d2s_aux.simps)+ |
|
1087 by (drule index_of_msg_le_length', simp) |
|
1088 |
|
1089 lemma cim2im_s_le_len: "cim2im_s \<tau> im = SCrea (Suc (length \<tau>)) \<Longrightarrow> False" |
|
1090 apply (simp add:cim2im_s_def, case_tac "inum2ind \<tau> im") |
|
1091 apply (simp add:d2s_aux.simps)+ |
|
1092 by (drule inum2ind_le_length', simp) |
|
1093 |
|
1094 lemma cfd2fd_s_le_len: "cfd2fd_s \<tau> p fd = SCrea (Suc (length \<tau>)) \<Longrightarrow> False" |
|
1095 apply (simp add:cfd2fd_s_def, case_tac "index_of_fd \<tau> p fd") |
|
1096 apply (simp add:d2s_aux.simps)+ |
|
1097 by (drule index_of_fd_le_length', simp) |
|
1098 |
1008 |
1099 end |
1009 end |
1100 |
1010 |
1101 (*<*) |
1011 (*<*) |
1102 end |
1012 end |