equal
deleted
inserted
replaced
246 and sproc: "cp2sproc s p = Some (r, fr, pt, u)" |
246 and sproc: "cp2sproc s p = Some (r, fr, pt, u)" |
247 using prem'[where obj = "Proc p"] vs |
247 using prem'[where obj = "Proc p"] vs |
248 by (auto split:option.splits if_splits simp:obj2sobj.simps |
248 by (auto split:option.splits if_splits simp:obj2sobj.simps |
249 dest:current_proc_has_sproc) |
249 dest:current_proc_has_sproc) |
250 have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os |
250 have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os |
251 apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits) |
251 apply (auto simp:obj2sobj.simps split:option.splits) |
252 apply (rule ai_cipc) using SP sproc rc ev by auto |
252 apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+) |
|
253 using SP sproc rc ev |
|
254 by (auto intro:ai_cipc) |
253 with True show ?thesis by simp |
255 with True show ?thesis by simp |
254 next |
256 next |
255 case False |
257 case False |
256 hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs |
258 hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs |
257 by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps |
259 by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps |
269 and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp" |
271 and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp" |
270 using prem'[where obj = "Proc p"] vs |
272 using prem'[where obj = "Proc p"] vs |
271 by (auto split:option.splits if_splits simp:obj2sobj.simps |
273 by (auto split:option.splits if_splits simp:obj2sobj.simps |
272 dest:current_proc_has_sproc) |
274 dest:current_proc_has_sproc) |
273 have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os |
275 have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os |
274 apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits) |
276 apply (auto simp:obj2sobj.simps split:option.splits) |
275 apply (rule ap_crole) using SP sproc rc ev srproc by auto |
277 apply (rule ap_crole) using SP sproc rc ev srproc by auto |
276 with True show ?thesis by simp |
278 with True show ?thesis by simp |
277 next |
279 next |
278 case False |
280 case False |
279 hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs |
281 hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs |
650 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
652 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
651 |
653 |
652 have valid: "valid (e # \<tau>)" |
654 have valid: "valid (e # \<tau>)" |
653 proof- |
655 proof- |
654 have "os_grant \<tau> e" |
656 have "os_grant \<tau> e" |
655 using ev tau expab by (simp) |
657 using ev tau expab by (simp add:ni_notin_curi) |
656 moreover have "rc_grant \<tau> e" |
658 moreover have "rc_grant \<tau> e" |
657 using ev tau ai'_cipc(3) SPab |
659 using ev tau ai'_cipc(3) SPab |
658 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
660 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
659 ultimately show ?thesis using vsab tau |
661 ultimately show ?thesis using vsab tau |
660 by (rule_tac vs_step, simp+) |
662 by (rule_tac vs_step, simp+) |
1177 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
1179 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
1178 |
1180 |
1179 have valid: "valid (e # \<tau>)" |
1181 have valid: "valid (e # \<tau>)" |
1180 proof- |
1182 proof- |
1181 have "os_grant \<tau> e" |
1183 have "os_grant \<tau> e" |
1182 using ev tau expab by (simp) |
1184 using ev tau expab by (simp add:ni_notin_curi) |
1183 moreover have "rc_grant \<tau> e" |
1185 moreover have "rc_grant \<tau> e" |
1184 using ev tau ai'_cipc(3) SPab |
1186 using ev tau ai'_cipc(3) SPab |
1185 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1187 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1186 ultimately show ?thesis using vsab tau |
1188 ultimately show ?thesis using vsab tau |
1187 by (rule_tac vs_step, simp+) |
1189 by (rule_tac vs_step, simp+) |
1303 by (auto simp:np_notin_curp) |
1305 by (auto simp:np_notin_curp) |
1304 |
1306 |
1305 have valid: "valid (e#\<tau>)" |
1307 have valid: "valid (e#\<tau>)" |
1306 proof- |
1308 proof- |
1307 have "os_grant \<tau> e" |
1309 have "os_grant \<tau> e" |
1308 using ev tau exp by (simp) |
1310 using ev tau exp by (simp add:np_notin_curp) |
1309 moreover have "rc_grant \<tau> e" |
1311 moreover have "rc_grant \<tau> e" |
1310 using ev tau ap'_crole(3) SPab |
1312 using ev tau ap'_crole(3) SPab |
1311 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1313 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1312 ultimately show ?thesis using vs_tau |
1314 ultimately show ?thesis using vs_tau |
1313 by (erule_tac vs_step, simp+) |
1315 by (erule_tac vs_step, simp+) |
1418 by (auto simp:np_notin_curp) |
1420 by (auto simp:np_notin_curp) |
1419 |
1421 |
1420 have valid: "valid (e#\<tau>)" |
1422 have valid: "valid (e#\<tau>)" |
1421 proof- |
1423 proof- |
1422 have "os_grant \<tau> e" |
1424 have "os_grant \<tau> e" |
1423 using ev tau exp ap'_chown(3) by (simp) |
1425 using ev tau exp ap'_chown(3) by (simp add:np_notin_curp) |
1424 moreover have "rc_grant \<tau> e" |
1426 moreover have "rc_grant \<tau> e" |
1425 using ev tau ap'_chown(5) SPab |
1427 using ev tau ap'_chown(5) SPab |
1426 by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange |
1428 by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange |
1427 split:option.splits t_rc_proc_type.splits) |
1429 split:option.splits t_rc_proc_type.splits) |
1428 (* here is another place of no_limit of clone event assumption *) |
1430 (* here is another place of no_limit of clone event assumption *) |
1925 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
1927 obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto |
1926 |
1928 |
1927 have valid: "valid (e # \<tau>)" |
1929 have valid: "valid (e # \<tau>)" |
1928 proof- |
1930 proof- |
1929 have "os_grant \<tau> e" |
1931 have "os_grant \<tau> e" |
1930 using ev tau expab by (simp) |
1932 using ev tau expab by (simp add:ni_notin_curi) |
1931 moreover have "rc_grant \<tau> e" |
1933 moreover have "rc_grant \<tau> e" |
1932 using ev tau ai'_cipc(3) SPab |
1934 using ev tau ai'_cipc(3) SPab |
1933 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1935 by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) |
1934 ultimately show ?thesis using vsab tau |
1936 ultimately show ?thesis using vsab tau |
1935 by (rule_tac vs_step, simp+) |
1937 by (rule_tac vs_step, simp+) |