Co2sobj_prop.thy
changeset 17 570f90f175ee
parent 16 c8b7c24f1db6
child 18 9b42765ce554
equal deleted inserted replaced
16:c8b7c24f1db6 17:570f90f175ee
  1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve
  1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve
  1101   cph2spshs_exit cph2spshs_kill cph2spshs_other
  1101   cph2spshs_exit cph2spshs_kill cph2spshs_other
  1102 
  1102 
  1103 (******** cp2sproc simpset *********)
  1103 (******** cp2sproc simpset *********)
  1104 
  1104 
  1105 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"
  1105 lemma not_init_intro_proc: (*???*)
  1106 apply (simp add:cp2sproc_def)
  1106   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
  1107 by (simp add:cp2sproc_def index_of_proc.simps)
  1107 using not_deleted_init_proc by auto
  1108 
  1108 
  1109 lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"
  1109 lemma not_init_intro_proc': (*???*)
  1110 by (simp add:cp2sproc_nil current_procs.simps)
  1110   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
  1111 
  1111 using not_deleted_init_proc by auto
  1112 lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (
  1112 
  1113                          if (p'' = p') then SCrea (Suc (length \<tau>))
  1113 lemma cp2sproc_clone:
  1114                          else cp2sproc \<tau> p''           )"
  1114   "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := 
  1115 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
  1115      case (sectxt_of_obj s (O_proc p)) of 
  1116 
  1116        Some sec \<Rightarrow> Some (Created, sec, 
  1117 lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"
  1117   {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd},
       
  1118   {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag})
       
  1119      | _        \<Rightarrow> None)"
       
  1120 apply (frule cph2spshs_clone, frule cpfd2sfds_clone)
       
  1121 apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps)
       
  1122 apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp)
       
  1123 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' 
       
  1124             dest:current_proc_has_sec split:option.splits if_splits)
       
  1125 done
       
  1126 
       
  1127 lemma cp2sproc_other:
       
  1128   "\<lbrakk>valid (e # s); 
       
  1129     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
       
  1130     \<forall> p fd. e \<noteq> CloseFd p fd;
       
  1131     \<forall> p h flag. e \<noteq> Attach p h flag;
       
  1132     \<forall> p h. e \<noteq> Detach p h;
       
  1133     \<forall> p h. e \<noteq> DeleteShM p h;
       
  1134     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
       
  1135     \<forall> p f fds. e \<noteq> Execve p f fds;
       
  1136     \<forall> p p'. e \<noteq> Kill p p';
       
  1137     \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s"
       
  1138 apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+)
       
  1139 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all) 
       
  1140 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' 
       
  1141             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1142 done
       
  1143 
       
  1144 lemma cp2sproc_open:
       
  1145   "valid (Open p f flags fd opt # s) \<Longrightarrow> 
       
  1146    cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p :=      
       
  1147      case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), 
       
  1148            cf2sfile (Open p f flags fd opt # s) f) of 
       
  1149        (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
       
  1150                                                then Init p else Created, sec, 
       
  1151                                                 (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p)
       
  1152      | _        \<Rightarrow> None)"
       
  1153 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
       
  1154 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)
       
  1155 apply (case_tac "x = p") 
       
  1156 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1157            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1158             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1159 done
       
  1160 
       
  1161 lemma cp2sproc_closefd:
       
  1162   "valid (CloseFd p fd # s) \<Longrightarrow> 
       
  1163    cp2sproc (CloseFd p fd # s) = (cp2sproc s) (p := 
       
  1164      if (fd \<in> proc_file_fds s p)
       
  1165      then (case (cfd2sfd s p fd) of 
       
  1166              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)
       
  1167                           then cp2sproc s p 
       
  1168                           else (case (sectxt_of_obj s (O_proc p)) of
       
  1169                                   Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
       
  1170                                                     then Init p else Created, 
       
  1171                                                     sec, cpfd2sfds s p - {sfd}, cph2spshs s p)
       
  1172                                 | _        \<Rightarrow> None))
       
  1173            | _        \<Rightarrow> cp2sproc s p)
       
  1174      else cp2sproc s p)"
       
  1175 apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
       
  1176 apply (frule vt_grant_os, frule vd_cons, rule ext)
       
  1177 apply (case_tac "x = p") 
       
  1178 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1179            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1180             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1181 done
       
  1182 
       
  1183 lemma cp2sproc_attach:
       
  1184   "valid (Attach p h flag # s) \<Longrightarrow> 
       
  1185    cp2sproc (Attach p h flag # s) = (cp2sproc s) (p := 
       
  1186      (case (ch2sshm s h) of 
       
  1187         Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of
       
  1188                       Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
       
  1189                                         then Init p else Created, 
       
  1190                                         sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)})
       
  1191                     | _        \<Rightarrow> None)
       
  1192       | _       \<Rightarrow> cp2sproc s p) )"
       
  1193 apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
       
  1194 apply (frule vt_grant_os, frule vd_cons, rule ext)
       
  1195 apply (case_tac "x = p") 
       
  1196 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1197            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1198             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1199 done
       
  1200 
       
  1201 lemma cp2sproc_detach:
       
  1202   "valid (Detach p h # s) \<Longrightarrow> 
       
  1203    cp2sproc (Detach p h # s) = (cp2sproc s) (p := 
       
  1204     (case (ch2sshm s h, flag_of_proc_shm s p h) of 
       
  1205        (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)
       
  1206                               then cp2sproc s p 
       
  1207                               else (case (sectxt_of_obj s (O_proc p)) of
       
  1208                                       Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
       
  1209                                                        then Init p else Created, sec,
       
  1210                                                        cpfd2sfds s p, cph2spshs s p - {(sh, flag)})
       
  1211                                     | None     \<Rightarrow> None)                   
       
  1212      | _       \<Rightarrow> cp2sproc s p)             )"
       
  1213 apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
       
  1214 apply (frule vt_grant_os, frule vd_cons, rule ext)
       
  1215 apply (case_tac "x = p") 
       
  1216 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1217            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1218             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1219 done
       
  1220 
       
  1221 lemma cp2sproc_deleteshm:
       
  1222   "valid (DeleteShM p h # s) \<Longrightarrow> 
       
  1223    cp2sproc (DeleteShM p h # s) = (\<lambda> p'. 
       
  1224     (case (ch2sshm s h, flag_of_proc_shm s p' h) of 
       
  1225        (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)
       
  1226                               then cp2sproc s p' 
       
  1227                               else (case (sectxt_of_obj s (O_proc p')) of
       
  1228                                       Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs) 
       
  1229                                                        then Init p' else Created, sec,
       
  1230                                                        cpfd2sfds s p', cph2spshs s p' - {(sh, flag)})
       
  1231                                     | None     \<Rightarrow> None)                   
       
  1232      | _       \<Rightarrow> cp2sproc s p')             )"
       
  1233 apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
       
  1234 apply (frule vt_grant_os, frule vd_cons, rule ext)
       
  1235 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1236            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1237             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1238 done
       
  1239 
       
  1240 lemma cp2sproc_execve:
       
  1241   "valid (Execve p f fds # s) \<Longrightarrow> 
       
  1242    cp2sproc (Execve p f fds # s) = (cp2sproc s) (p := 
       
  1243      (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of
       
  1244         Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
       
  1245                          {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {})
       
  1246       | _        \<Rightarrow> None)                        )"
       
  1247 apply (frule cph2spshs_execve, frule cpfd2sfds_execve)
       
  1248 apply (frule vt_grant_os, frule vd_cons, rule ext)
       
  1249 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1250            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1251             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1252 done
       
  1253 
       
  1254 lemma cp2sproc_kill:
       
  1255   "\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow> 
       
  1256    cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
       
  1257 apply (frule cph2spshs_kill, frule cpfd2sfds_kill)
       
  1258 apply (frule vt_grant_os, frule vd_cons)
       
  1259 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1260            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1261             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1262 done
       
  1263 
       
  1264 lemma cp2sproc_kill':
       
  1265   "\<lbrakk>valid (Kill p p' # s); p'' \<in> current_procs (Kill p p' # s)\<rbrakk> \<Longrightarrow> 
       
  1266    cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
       
  1267 by (drule_tac p'' = p'' in cp2sproc_kill, simp+)
       
  1268 
       
  1269 lemma cp2sproc_exit:
       
  1270   "\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> 
       
  1271    cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
       
  1272 apply (frule cph2spshs_exit, frule cpfd2sfds_exit)
       
  1273 apply (frule vt_grant_os, frule vd_cons)
       
  1274 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
       
  1275            dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
       
  1276             dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
       
  1277 done
       
  1278 
       
  1279 lemma cp2sproc_exit':
       
  1280   "\<lbrakk>valid (Exit p # s); p' \<in> current_procs (Exit p # s)\<rbrakk> \<Longrightarrow> 
       
  1281    cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
       
  1282 by (drule_tac p'= p' in cp2sproc_exit, simp+)
       
  1283 
       
  1284 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
       
  1285   cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other 
       
  1286 
       
  1287 (********************* cm2smsg simpset ***********************)
       
  1288 
       
  1289 lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
       
  1290 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
  1118 apply (case_tac e)
  1291 apply (case_tac e)
  1119 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
  1292 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits)
  1120 
       
  1121 lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other
       
  1122 
       
  1123 (********************* cm2smsg simpset ***********************)
       
  1124 
       
  1125 lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"
       
  1126 by (simp add:cm2smsg_def index_of_msg.simps)
       
  1127 
       
  1128 lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"
       
  1129 by (simp add:cm2smsg_nil current_msgs.simps)
       
  1130 
       
  1131 lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"
       
  1132 by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)
       
  1133 
       
  1134 lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"
       
  1135 apply (case_tac e)
       
  1136 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)
       
  1137 
  1293 
  1138 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
  1294 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
       
  1295 
       
  1296 
       
  1297 
       
  1298 (********************* cq2smsgq simpset ***********************) 
       
  1299 
       
  1300 lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
       
  1301 apply (case_tac e) 
       
  1302 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
       
  1303 
       
  1304 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
       
  1305 
  1139 
  1306 
  1140 
  1307 
  1141 
  1308 
  1142 end
  1309 end
  1143 
  1310