theory all_sobj_propimports Main rc_theory os_rc obj2sobj_prop deleted_prop sound_defs_prop source_propbegincontext tainting_s_complete beginlemma initf_has_effinitialrole: "f \<in> init_files ==> \<exists> r. effinitialrole [] f = Some r"by (rule_tac f = f in file_has_effinitialrole, simp, simp add:vs_nil)lemma initf_has_effforcedrole: "f \<in> init_files ==> \<exists> r. effforcedrole [] f = Some r"by (rule_tac f = f in file_has_effforcedrole, simp, simp add:vs_nil)lemma efffrole_sdir_some: "sd \<in> init_files ==> \<exists> r. erole_functor init_file_forcedrole InheritUpMixed sd = Some r"apply (frule_tac s = "[]" in undel_initf_keeps_efrole, simp, simp add:vs_nil)by (drule initf_has_effforcedrole, simp)lemma efffrole_sdir_some': "erole_functor init_file_forcedrole InheritUpMixed sd = None ==> sd \<notin> init_files"by (rule notI, auto dest!:efffrole_sdir_some)lemma effirole_sdir_some: "sd \<in> init_files ==> \<exists> r. erole_functor init_file_initialrole UseForcedRole sd = Some r"apply (frule_tac s = "[]" in undel_initf_keeps_eirole, simp, simp add:vs_nil)by (drule initf_has_effinitialrole, simp)lemma effirole_sdir_some': "erole_functor init_file_initialrole UseForcedRole sd = None ==> sd \<notin> init_files"by (rule notI, auto dest:effirole_sdir_some)lemma erole_func_irole_simp: "erole_functor init_file_initialrole UseForcedRole sd = effinitialrole [] sd"by (simp add:effinitialrole_def)lemma erole_func_frole_simp: "erole_functor init_file_forcedrole InheritUpMixed sd = effforcedrole [] sd"by (simp add:effforcedrole_def)lemma init_effforcedrole_valid: "erole_functor init_file_forcedrole InheritUpMixed sd = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"by (simp add:erole_func_frole_simp, erule effforcedrole_valid)lemma init_effinitialrole_valid: "erole_functor init_file_initialrole UseForcedRole sd = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" by (simp add:erole_func_irole_simp, erule effinitialrole_valid)lemma exec_role_some: "[|sd \<in> init_files; u \<in> init_users|] ==> \<exists> r'. exec_role_aux r sd u = Some r'"by (auto simp:exec_role_aux_def split:option.splits t_role.splits dest!:effirole_sdir_some' efffrole_sdir_some' dest:init_effforcedrole_valid init_effinitialrole_valid intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)lemma chown_role_some: "u \<in> init_users ==> \<exists> r'. chown_role_aux r fr u = Some r'"by (auto simp:chown_role_aux_def split:option.splits t_role.splits dest!:effirole_sdir_some' efffrole_sdir_some' dest:init_effforcedrole_valid init_effinitialrole_valid intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)declare obj2sobj.simps [simp del]lemma all_sobjs_I: assumes ex: "exists s obj" and vd: "valid s" shows "obj2sobj s obj \<in> all_sobjs"using ex vdproof (induct s arbitrary:obj) case Nil assume ex:"exists [] obj" show ?case proof (cases obj) case (Proc p) assume prem: "obj = Proc p" with ex have initp:"p \<in> init_processes" by simp from initp obtain r where "init_currentrole p = Some r" using init_proc_has_role by (auto simp:bidirect_in_init_def) moreover from initp obtain t where "init_process_type p = Some t" using init_proc_has_type by (auto simp:bidirect_in_init_def) moreover from initp obtain fr where "init_proc_forcedrole p = Some fr" using init_proc_has_frole by (auto simp:bidirect_in_init_def) moreover from initp obtain u where "init_owner p = Some u" using init_proc_has_owner by (auto simp:bidirect_in_init_def) ultimately have "obj2sobj [] (Proc p) \<in> all_sobjs" using initp by (auto intro!:ap_init simp:obj2sobj.simps) with prem show ?thesis by simp next case (File f) assume prem: "obj = File f" with ex have initf: "f \<in> init_files" by simp from initf obtain t where "etype_aux init_file_type_aux f = Some t" using init_file_has_etype by auto moreover from initf have "source_dir [] f = Some f" by (simp add:source_dir_of_init') ultimately have "obj2sobj [] (File f) \<in> all_sobjs" using initf by (auto simp:etype_of_file_def obj2sobj.simps intro!:af_init) with prem show ?thesis by simp next case (IPC i) assume prem: "obj = IPC i" with ex have initi: "i \<in> init_ipcs" by simp from initi obtain t where "init_ipc_type i = Some t" using init_ipc_has_type by (auto simp:bidirect_in_init_def) hence "obj2sobj [] (IPC i) \<in> all_sobjs" using initi by (auto intro!:ai_init simp:obj2sobj.simps) with prem show ?thesis by simp qednext case (Cons e s) assume prem: "\<And> obj. \<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<in> all_sobjs" and ex_cons: "exists (e # s) obj" and vs_cons: "valid (e # s)" have vs: "valid s" and rc: "rc_grant s e" and os: "os_grant s e" using vs_cons by (auto intro:valid_cons valid_os valid_rc) from prem and vs have prem': "\<And> obj. exists s obj \<Longrightarrow> obj2sobj s obj \<in> all_sobjs" by simp show ?case proof (cases e) case (ChangeOwner p u) assume ev: "e = ChangeOwner p u" show ?thesis proof (cases "obj = Proc p") case True have curp: "p \<in> current_procs s" and exp: "exists s (Proc p)" using os ev by auto from curp obtain r fr t u' srp where sp: "obj2sobj s (Proc p) = SProc (r,fr,t,u') (Some srp)" using vs apply (drule_tac current_proc_has_sobj, simp) by blast hence sp_in: "SProc (r,fr,t,u') (Some srp) \<in> all_sobjs" using prem' exp by metis have comp: "(r, Proc_type t, CHANGE_OWNER) \<in> compatible" using sp ev rc by (auto simp:obj2sobj.simps split:option.splits) from os ev have uinit: "u \<in> init_users" by simp then obtain nr where chown: "chown_role_aux r fr u = Some nr" by (auto dest:chown_role_some) hence nsp_in:"obj2sobj (e#s) (Proc p) = SProc (nr,fr,chown_type_aux r nr t, u) (Some srp)" using sp ev os by (auto split:option.splits t_role.splits simp del:currentrole.simps type_of_process.simps simp add:chown_role_aux_valid chown_type_aux_valid obj2sobj.simps) thus ?thesis using True ev os rc sp_in sp by (auto simp:chown comp intro!:ap_chown[where u'=u']) next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (Clone p p') assume ev: "e = Clone p p'" show ?thesis proof (cases "obj = Proc p'") case True from ev os have exp: "exists s (Proc p)" by (simp add:os_grant.simps) from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srp: "source_proc s p = Some sp" using vs apply (simp del:cp2sproc.simps) by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast) hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs by (auto split:option.splits simp add:obj2sobj.simps) have "obj2sobj (e # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)" using ev sproc srp vs_cons by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps) thus ?thesis using True SP by (simp add:ap_clone) next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (Execute p f) assume ev: "e = Execute p f" show ?thesis proof (cases "obj = Proc p") case True from ev os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srp: "source_proc s p = Some sp" using vs apply (simp del:cp2sproc.simps) by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast) hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs by (auto split:option.splits simp add:obj2sobj.simps) from exf obtain sd t where srdir: "source_dir s f = Some sd" and etype: "etype_of_file s f = Some t" using vs by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype) then obtain srf where SF: "SFile (t, sd) srf \<in> all_sobjs" using exf prem'[where obj = "File f"] vs by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_file_has_etype) from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs by (auto intro:source_dir_in_init owner_in_users split:option.splits) then obtain nr where "exec_role_aux r sd u = Some nr" by (auto dest:exec_role_some) hence "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons srdir sproc srp apply (auto simp:obj2sobj.simps cp2sproc_simps source_proc.simps intro:source_dir_in_init simp del:cp2sproc.simps split:option.splits dest!:efffrole_sdir_some') apply (rule ap_exec) using SF SP rc ev etype by (auto split:option.splits) with True show ?thesis by simp next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (CreateFile p f) assume ev: "e = CreateFile p f" show ?thesis proof (cases "obj = File f") case True from os ev obtain pf where expf: "exists s (File pf)" and parent:"parent f = Some pf" by auto from expf obtain pft sd srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs" and eptype: "etype_of_file s pf = Some pft" and srpf: "source_dir s pf = Some sd" using prem'[where obj = "File pf"] vs by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_file_has_etype current_file_has_sd) from os ev have exp: "exists s (Proc p)" by simp then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs" and sproc: "cp2sproc s p = Some (r, fr, pt, u)" using prem'[where obj = "Proc p"] vs by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_proc_has_sproc) have "obj2sobj (e # s) (File f) \<in> all_sobjs" using ev vs_cons sproc srpf parent os apply (auto simp:obj2sobj.simps source_dir_simps init_notin_curf_deleted split:option.splits dest!:current_file_has_etype') apply (case_tac "default_fd_create_type r") using SF SP rc ev eptype sproc apply (rule_tac sf = srpf in af_cfd', auto simp:etype_of_file_def etype_aux_prop3) [1] using SF SP rc ev eptype sproc apply (rule_tac sf = srpf in af_cfd) apply (auto simp:etype_of_file_def etype_aux_prop4) done with True show ?thesis by simp next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps etype_aux_prop2 split:option.splits t_role.splits ) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (CreateIPC p i) assume ev: "e = CreateIPC p i" show ?thesis proof (cases "obj = IPC i") case True from os ev have exp: "exists s (Proc p)" by simp then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs" and sproc: "cp2sproc s p = Some (r, fr, pt, u)" using prem'[where obj = "Proc p"] vs by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_proc_has_sproc) have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os apply (auto simp:obj2sobj.simps split:option.splits) apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+) using SP sproc rc ev by (auto intro:ai_cipc) with True show ?thesis by simp next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits ) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (ChangeRole p r') assume ev: "e = ChangeRole p r'" show ?thesis proof (cases "obj = Proc p") case True from os ev have exp: "exists s (Proc p)" by simp then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs" and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp" using prem'[where obj = "Proc p"] vs by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_proc_has_sproc) have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os apply (auto simp:obj2sobj.simps split:option.splits) apply (rule ap_crole) using SP sproc rc ev srproc by auto with True show ?thesis by simp next case False hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits ) thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto) qed next case (ReadFile p f) assume ev: "e = ReadFile p f" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) moreover have "exists s obj" using ev ex_cons by (case_tac obj, auto) ultimately show ?thesis using prem[where obj = obj] vs by simp next case (WriteFile p f) assume ev: "e = WriteFile p f" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) moreover have "exists s obj" using ev ex_cons by (case_tac obj, auto) ultimately show ?thesis using prem[where obj = obj] vs by simp next case (Send p i) assume ev: "e = Send p i" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) moreover have "exists s obj" using ev ex_cons by (case_tac obj, auto) ultimately show ?thesis using prem[where obj = obj] vs by simp next case (Recv p i) assume ev: "e = Recv p i" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) moreover have "exists s obj" using ev ex_cons by (case_tac obj, auto) ultimately show ?thesis using prem[where obj = obj] vs by simp next case (Kill p p') assume ev: "e = Kill p p'" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) thus ?thesis using prem[where obj = obj] vs ex_cons ev by (case_tac obj, auto) next case (DeleteFile p f') assume ev: "e = DeleteFile p f'" have "obj2sobj (e#s) obj = obj2sobj s obj" proof- have "\<And> f. obj = File f ==> obj2sobj (e#s) (File f) = obj2sobj s (File f)" using ev vs os ex_cons vs_cons by (auto simp:obj2sobj.simps etype_of_file_delete source_dir_simps split:option.splits t_role.splits if_splits dest!:current_file_has_etype' current_file_has_sd' dest:source_dir_prop) moreover have "\<forall> f. obj \<noteq> File f ==> obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps split:option.splits) ultimately show ?thesis by auto qed thus ?thesis using prem[where obj = obj] vs ex_cons ev by (case_tac obj, auto) next case (DeleteIPC p i) assume ev: "e = DeleteIPC p i" have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps split:option.splits t_role.splits) thus ?thesis using prem[where obj = obj] vs ex_cons ev by (case_tac obj, auto) qedqeddeclare obj2sobj.simps [simp add]lemma seeds_in_all_sobjs: assumes seed: "obj \<in> seeds" shows "init_obj2sobj obj \<in> all_sobjs"proof (cases obj) case (Proc p) assume p0: "obj = Proc p" (*?*) from seed p0 have pinit: "p \<in> init_processes" by (drule_tac seeds_in_init, simp) from pinit obtain r where "init_currentrole p = Some r" using init_proc_has_role by (auto simp:bidirect_in_init_def) moreover from pinit obtain fr where "init_proc_forcedrole p = Some fr" using init_proc_has_frole by (auto simp:bidirect_in_init_def) moreover from pinit obtain pt where "init_process_type p = Some pt" using init_proc_has_type by (auto simp:bidirect_in_init_def) moreover from pinit obtain u where "init_owner p = Some u" using init_proc_has_owner by (auto simp:bidirect_in_init_def) ultimately show ?thesis using p0 by (auto intro:ap_init)next case (File f) assume p0: "obj = File f" (*?*) from seed p0 have finit: "f \<in> init_files" by (drule_tac seeds_in_init, simp) then obtain t where "etype_aux init_file_type_aux f = Some t" by (auto dest:init_file_has_etype) with finit p0 show ?thesis by (auto intro:af_init)next case (IPC i) assume p0: "obj = IPC i" (*?*) from seed p0 have iinit: "i \<in> init_ipcs" by (drule_tac seeds_in_init, simp) then obtain t where "init_ipc_type i = Some t" using init_ipc_has_type by (auto simp:bidirect_in_init_def) with iinit p0 show ?thesis by (auto intro:ai_init)qedlemma tainted_s_in_all_sobjs: "sobj \<in> tainted_s \<Longrightarrow> sobj \<in> all_sobjs"apply (erule tainted_s.induct)apply (erule seeds_in_all_sobjs)apply (auto intro:ap_crole ap_exec ap_chown ai_cipc af_cfd af_cfd' ap_clone)doneendcontext tainting_s_sound begin(*** all_sobjs' equal with all_sobjs in the view of soundness ***)lemma all_sobjs'_eq1: "sobj \<in> all_sobjs \<Longrightarrow> sobj \<in> all_sobjs'"apply (erule all_sobjs.induct)apply (auto intro:af'_init af'_cfd af'_cfd' ai'_init ai'_cipc ap'_init ap'_crole ap'_exec ap'_chown)by (simp add:clone_type_aux_def clone_type_unchange)lemma all_sobjs'_eq2: "sobj \<in> all_sobjs' \<Longrightarrow> sobj \<in> all_sobjs"apply (erule all_sobjs'.induct)by (auto intro:af_init af_cfd af_cfd' ai_init ai_cipc ap_init ap_crole ap_exec ap_chown)lemma all_sobjs'_eq: "(sobj \<in> all_sobjs) = (sobj \<in> all_sobjs')"by (auto intro:iffI all_sobjs'_eq1 all_sobjs'_eq2)(************************ all_sobjs Elim Rules ********************)declare obj2sobj.simps [simp del]declare cp2sproc.simps [simp del]lemma all_sobjs_E0_aux[rule_format]: "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"proof (induct rule:all_sobjs'.induct) case (af'_init f t) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact s'" and exso': "exists s' obj'" from nodels' af'_init(1) have exf: "f \<in> current_files s'" by (drule_tac obj = "File f" in nodel_imp_exists, simp+) have "obj2sobj s' (File f) = SFile (t, f) (Some f)" proof- have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps split:option.splits) thus ?thesis using vss' exf nodels' af'_init(1) by (drule_tac obj2sobj_file_remains_app', auto) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI) by (simp add:vss' sobjs' nodels' intacts' exf exso') qednext case (af'_cfd t sd srf r fr pt u srp t') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact (sa@s')" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd(3,4) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact (sb@sa@s')" and nodelab: "no_del_event (sb@sa@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd(5,6,7) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp_all add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'" using ev tau SFab SPab af'_cfd(5) by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def split:option.splits if_splits intro!:etype_aux_prop4) moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj " using tau ev by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+) qednext case (af'_cfd' t sd srf r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd'(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact (sa@s')" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd'(3,4) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact (sb@sa@s')" and nodelab: "no_del_event (sb@sa@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd'(5,6) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf" using ev tau SPab af'_cfd'(5) by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps split:option.splits intro!:etype_aux_prop3) thus ?thesis using SFab tau ev by (auto simp:obj2sobj.simps split:option.splits if_splits) qed moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj" using tau ev by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+) qed next case (ai'_init i t) hence initi: "i \<in> init_ipcs" using init_ipc_has_type by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact s'" and exso': "exists s' obj'" from nodels' initi have exi: "i \<in> current_ipcs s'" by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+) have "obj2sobj s' (IPC i) = SIPC t (Some i)" proof- have "obj2sobj [] (IPC i) = SIPC t (Some i)" using ai'_init initi by (auto simp:obj2sobj.simps) thus ?thesis using vss' exi nodels' initi by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI) by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps) qednext case (ai'_cipc r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with ai'_cipc(1,2) notUkn obtain s p where SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and soab: "obj2sobj (s@s') obj' = sobj'" and exsoab: "exists (s@s') obj'" and intactab: "initp_intact (s@s')" and nodelab: "no_del_event (s@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab by (simp add:ni_notin_curi) moreover have "rc_grant \<tau> e" using ev tau ai'_cipc(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None" using ev tau SPab nodel nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps split:option.splits dest:no_del_event_cons_D) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj" using tau ev by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, simp+) qed next case (ap'_init p r fr t u) hence initp: "p \<in> init_processes" using init_proc_has_role by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'" and Nodels': "no_del_event s'"and Intacts':"initp_intact s'" and exso': "exists s' obj'" from Nodels' initp have exp: "p \<in> current_procs s'" apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted) by (drule not_deleted_imp_exists, simp+) with Intacts' initp ap'_init have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)" by (auto simp:initp_intact_def split:option.splits) thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI) by (simp add:VSs' SOs' Nodels' exp exso' initp intact_imp_butp Intacts' del:obj2sobj.simps) qednext case (ap'_crole r fr t u srp r') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_crole(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and intactab: "initp_intact (s@s')" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp) moreover have "rc_grant \<tau> e" using ev tau ap'_crole(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact (e#\<tau>)" using tau ev intactab valid by (simp add:initp_intact_I_crole) moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (s @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp" using SPab tau vs_tau ev valid by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto) qednext case (ap'_chown r fr t u srp u' nr) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_chown(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and intactab: "initp_intact (s@s')" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp ap'_chown(3) by (simp) moreover have "rc_grant \<tau> e" using ev tau ap'_chown(5) SPab by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange split:option.splits t_rc_proc_type.splits) (* here is another place of no_limit of clone event assumption *) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid by (simp add:initp_intact_I_chown) moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (s @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (nr,fr,chown_type_aux r nr t,u') srp" using SPab tau vs_tau ev valid ap'_chown(4) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto) qednext case (ap'_exec r fr pt u sp t sd sf r' fr') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_exec(3,4) obtain sa f where SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and Exfa: "exists (sa @ s') (File f)" and butsa: "initp_intact (sa @ s')" and othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> exists (sa @s') obj' \<and> no_del_event (sa @ s')" by (blast dest:obj2sobj_file intro:nodel_exists_remains) with ap'_exec(1,2) notUkn obtain sb p where VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'" and nodelab: "no_del_event (sb@sa@s')" and intactab: "initp_intact (sb@sa@s')" and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp" and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f" and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File f" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp add:exf) moreover have "rc_grant \<tau> e" using ev tau ap'_exec(5) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact (e#\<tau>)" using tau ev intactab valid by (simp add:initp_intact_I_exec) moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (sb @ sa @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) = SProc (r',fr',exec_type_aux r pt, u) sp" proof- have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps) hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange split:option.splits) moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits) ultimately show ?thesis using valid ev ap'_exec(6,7) by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI) by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto) qedqed(* this is for ts2t createfile case ... *)lemma all_sobjs_E0: "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; no_del_event s'; initp_intact s'\<rbrakk> \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"by (drule all_sobjs_E0_aux, auto)lemma all_sobjs_E1_aux[rule_format]: "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact_but s' sobj' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"proof (induct rule:all_sobjs'.induct) case (af'_init f t) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'" and exso': "exists s' obj'" from nodels' af'_init(1) have exf: "f \<in> current_files s'" by (drule_tac obj = "File f" in nodel_imp_exists, simp+) have "obj2sobj s' (File f) = SFile (t, f) (Some f)" proof- have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps split:option.splits) thus ?thesis using vss' exf nodels' af'_init(1) by (drule_tac obj2sobj_file_remains_app', auto) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI) by (simp add:vss' sobjs' nodels' intacts' exf exso') qednext case (af'_cfd t sd srf r fr pt u srp t') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd(3,4) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact_but (sb@sa@s') sobj'" and nodelab: "no_del_event (sb@sa@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd(5,6,7) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'" using ev tau SFab SPab af'_cfd(5) by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def split:option.splits if_splits intro!:etype_aux_prop4) moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed moreover have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel apply (case_tac sobj', case_tac option) by (simp_all add:initp_intact_butp_I_others initp_intact_I_others) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj " using tau ev apply (rule_tac x = "e#sb@sa" in exI) by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto) qednext case (af'_cfd' t sd srf r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd'(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd'(3,4) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact_but (sb@sa@s') sobj'" and nodelab: "no_del_event (sb@sa@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd'(5,6) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf" using ev tau SPab af'_cfd'(5) by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def split:option.splits intro!:etype_aux_prop3) thus ?thesis using SFab tau ev by (auto simp:obj2sobj.simps split:option.splits if_splits) qed moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed moreover have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel apply (case_tac sobj', case_tac option) by (simp_all add:initp_intact_butp_I_others initp_intact_I_others) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj" using tau ev apply (rule_tac x = "e#sb@sa" in exI) by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto) qed next case (ai'_init i t) hence initi: "i \<in> init_ipcs" using init_ipc_has_type by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'" and exso': "exists s' obj'" from nodels' initi have exi: "i \<in> current_ipcs s'" by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+) have "obj2sobj s' (IPC i) = SIPC t (Some i)" proof- have "obj2sobj [] (IPC i) = SIPC t (Some i)" using ai'_init initi by (auto simp:obj2sobj.simps) thus ?thesis using vss' exi nodels' initi by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI) by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps) qednext case (ai'_cipc r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with ai'_cipc(1,2) notUkn obtain s p where SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and soab: "obj2sobj (s@s') obj' = sobj'" and exsoab: "exists (s@s') obj'" and intactab: "initp_intact_but (s@s') sobj'" and nodelab: "no_del_event (s@s')" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab by (simp add:ni_notin_curi) moreover have "rc_grant \<tau> e" using ev tau ai'_cipc(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None" using ev tau SPab nodel nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps split:option.splits dest:no_del_event_cons_D) moreover have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel apply (case_tac sobj', case_tac option) by (simp_all add:initp_intact_butp_I_others initp_intact_I_others) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj" using tau ev by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto) qed next case (ap'_init p r fr t u) (* the big difference from other elims is in this case *) hence initp: "p \<in> init_processes" using init_proc_has_role by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'" and Nodels': "no_del_event s'"and Intacts':"initp_intact_but s' sobj'" and exso': "exists s' obj'" and notUkn: "sobj' \<noteq> Unknown" from Nodels' initp have exp: "p \<in> current_procs s'" by (drule_tac obj = "Proc p" in nodel_imp_exists, simp+) have "\<exists> p'. obj2sobj s' (Proc p') = SProc (r,fr,t,u) (Some p) \<and> p' \<in> current_procs s'" proof (cases sobj') case (SProc sp srp) show ?thesis proof (cases srp) case None with SProc Intacts' have "initp_intact s'" by simp thus ?thesis using initp ap'_init apply (rule_tac x = p in exI) by (auto simp:initp_intact_def exp split:option.splits) next case (Some p') show ?thesis proof (cases "p' = p") case True with Intacts' SProc Some have "initp_alter s' p" by (simp add:initp_intact_butp_def) then obtain pa where "pa \<in> current_procs s'" and "obj2sobj s' (Proc pa) = init_obj2sobj (Proc p)" by (auto simp only:initp_alter_def) thus ?thesis using ap'_init initp by (rule_tac x = pa in exI, auto) next case False with Intacts' SProc Some initp have "obj2sobj s' (Proc p) = init_obj2sobj (Proc p)" apply (simp only:initp_intact_butp_def initp_intact_but.simps) by (erule conjE, erule_tac x = p in allE, simp) thus ?thesis using ap'_init exp by (rule_tac x = p in exI, auto split:option.splits) qed qed next case (SFile sf srf) thus ?thesis using ap'_init exp Intacts' initp by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def) next case (SIPC si sri) thus ?thesis using ap'_init exp Intacts' initp by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def) next case Unknown thus ?thesis using notUkn by simp qed then obtain p' where "obj2sobj s' (Proc p') = SProc (r, fr, t, u) (Some p)" and "p' \<in> current_procs s'" by blast thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj" apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p'" in exI) by (simp add:VSs' SOs' Nodels' exp exso' Intacts') qed next case (ap'_crole r fr t u srp r') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_crole(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and intactab: "initp_intact_but (s@s') sobj'" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists) by (auto simp:np_notin_curp) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp add:np_notin_curp) moreover have "rc_grant \<tau> e" using ev tau ap'_crole(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) sobj'" proof (cases sobj') case (SProc sp srp) show ?thesis proof (cases srp) case (Some p') with SOab' exobj'ab VSab intactab notUkn SProc have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'" by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps split:if_splits option.splits) then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')" by (auto simp:initp_alter_def initp_intact_butp_def) hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel apply (simp add:initp_alter_def del:init_obj2sobj.simps) apply (rule_tac x = p'' in exI, rule conjI, simp) apply (subgoal_tac "p'' \<noteq> new_proc (s @s')") apply (auto simp:obj2sobj.simps cp2sproc.simps simp del:init_obj2sobj.simps split:option.splits)[1] by (rule notI, simp add:np_notin_curp) thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps) apply (rule impI|rule allI|rule conjI|erule conjE)+ apply (erule_tac x = pa in allE) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps split:option.splits) next case None with intactab SProc have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_crole) thus ?thesis using SProc None by simp qed next case (SFile sf srf) with intactab SFile have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_crole) thus ?thesis using SFile by simp next case (SIPC si sri) with intactab SIPC have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_crole) thus ?thesis using SIPC by simp next case Unknown with notUkn show ?thesis by simp qed moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (s @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp" using SPab tau vs_tau ev valid by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto) qed next case (ap'_chown r fr t u srp u' nr) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_chown(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and intactab: "initp_intact_but (s@s') sobj'" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists) by (auto simp:np_notin_curp) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp ap'_chown(3) by (simp add:np_notin_curp) moreover have "rc_grant \<tau> e" using ev tau ap'_chown(5) SPab by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange split:option.splits t_rc_proc_type.splits) (* here is another place of no_limit of clone event assumption *) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) sobj'" proof (cases sobj') case (SProc sp srp) show ?thesis proof (cases srp) case (Some p') with SOab' exobj'ab VSab intactab notUkn SProc have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'" by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps split:if_splits option.splits) then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')" by (auto simp:initp_alter_def initp_intact_butp_def) hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel apply (simp add:initp_alter_def del:init_obj2sobj.simps) apply (rule_tac x = p'' in exI, rule conjI, simp) apply (subgoal_tac "p'' \<noteq> new_proc (s @s')") apply (auto simp:obj2sobj.simps cp2sproc.simps simp del:init_obj2sobj.simps split:option.splits)[1] by (rule notI, simp add:np_notin_curp) thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps) apply (rule impI|rule allI|rule conjI|erule conjE)+ apply (erule_tac x = pa in allE) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps split:option.splits) next case None with intactab SProc have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_chown) thus ?thesis using SProc None by simp qed next case (SFile sf srf) with intactab SFile have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_chown) thus ?thesis using SFile by simp next case (SIPC si sri) with intactab SIPC have "initp_intact (s@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_chown) thus ?thesis using SIPC by simp next case Unknown with notUkn show ?thesis by simp qed moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (s @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (nr,fr,chown_type_aux r nr t,u') srp" using SPab tau vs_tau ev valid ap'_chown(4) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto) qednext case (ap'_exec r fr pt u sp t sd sf r' fr') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_exec(3,4) obtain sa f where SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and Exfa: "exists (sa @ s') (File f)" and butsa: "initp_intact_but (sa @ s') sobj'" and othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> exists (sa @s') obj' \<and> no_del_event (sa @ s')" by (blast dest:obj2sobj_file intro:nodel_exists_remains) with ap'_exec(1,2) notUkn obtain sb p where VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'" and nodelab: "no_del_event (sb@sa@s')" and intactab: "initp_intact_but (sb@sa@s') sobj'" and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp" and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'" by (blast dest:obj2sobj_proc intro:nodel_exists_remains) obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f" and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File f" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all) have np_not_initp: "new_proc (sb@sa@s') \<notin> init_processes" using nodelab apply (rule_tac notI, drule_tac obj = "Proc (new_proc (sb@sa@s'))" in nodel_imp_exists) by (auto simp:np_notin_curp) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp add:exf) moreover have "rc_grant \<tau> e" using ev tau ap'_exec(5) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) sobj'" proof (cases sobj') case (SProc sp srp) show ?thesis proof (cases srp) case (Some p') with SOab' exobj'ab VSab intactab notUkn SProc have butp: "p' \<in> init_processes \<and> initp_intact_butp (sb@sa@s') p'" by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps split:if_splits option.splits) then obtain p'' where exp': "p'' \<in> current_procs (sb@sa@s')" and SP': "obj2sobj (sb@sa@s') (Proc p'') = init_obj2sobj (Proc p')" by (auto simp:initp_alter_def initp_intact_butp_def) hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel apply (simp add:initp_alter_def del:init_obj2sobj.simps) apply (rule_tac x = p'' in exI, rule conjI, simp) apply (subgoal_tac "p'' \<noteq> new_proc (sb@sa@s')") apply (auto simp:obj2sobj.simps cp2sproc.simps simp del:init_obj2sobj.simps split:option.splits)[1] by (rule notI, simp add:np_notin_curp) thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps) apply (rule impI|rule allI|rule conjI|erule conjE)+ apply (erule_tac x = pa in allE) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps split:option.splits) next case None with intactab SProc have "initp_intact (sb@sa@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_exec) thus ?thesis using SProc None by simp qed next case (SFile sf srf) with intactab SFile have "initp_intact (sb@sa@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_exec) thus ?thesis using SFile by simp next case (SIPC si sri) with intactab SIPC have "initp_intact (sb@sa@s')" by simp hence "initp_intact (e#\<tau>)" using tau ev valid by (simp add:initp_intact_I_exec) thus ?thesis using SIPC by simp next case Unknown with notUkn show ?thesis by simp qed moreover have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" apply (case_tac "p' = new_proc (sb @ sa @ s')") using vs_tau exobj'ab tau apply (simp, drule_tac valid_os, simp add:np_notin_curp) using tau ev SOab' valid notUkn vs_tau by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) = SProc (r',fr',exec_type_aux r pt, u) sp" proof- have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps) hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange split:option.splits) moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits) ultimately show ?thesis using valid ev ap'_exec(6,7) by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and> exists (s @ s') obj" using ev tau apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI) by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto) qedqed(* this is for all_sobjs_E2 *)lemma all_sobjs_E1: "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; no_del_event s'; initp_intact_but s' sobj'\<rbrakk> \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"by (drule all_sobjs_E1_aux, auto)lemma all_sobjs_E2_aux[rule_format]: "sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> not_both_sproc sobj sobj' \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and> sobj_source_eq_obj sobj obj))"proof (induct rule:all_sobjs'.induct) case (af'_init f t) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact s'" and notboth: "not_both_sproc (SFile (t, f) (Some f)) sobj'" and exso': "exists s' obj'" from nodels' af'_init(1) have exf: "f \<in> current_files s'" by (drule_tac obj = "File f" in nodel_imp_exists, simp+) have "obj2sobj s' (File f) = SFile (t, f) (Some f)" proof- have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps split:option.splits) thus ?thesis using vss' exf nodels' af'_init(1) by (drule_tac obj2sobj_file_remains_app', auto) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SFile (t, f) (Some f)) \<and> obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, f) (Some f)) obj" apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI) by (simp add:vss' sobjs' nodels' intacts' exf exso') qednext case (af'_cfd t sd srf r fr pt u srp t') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SFile (t', sd) None) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact (sa@s')" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file) apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd(3) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact (sb@sa@s')" and nodelab: "no_del_event (sb@sa@s')" apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto) apply (frule obj2sobj_proc, erule exE) by (auto intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd(5,6,7) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'" using ev tau SFab SPab af'_cfd(5) by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps split:option.splits if_splits intro!:etype_aux_prop4) moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SFile (t', sd) None) \<and> obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t', sd) None) obj" using tau ev apply (rule_tac x = "e#sb@sa" in exI) by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto) qednext case (af'_cfd' t sd srf r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SFile (t, sd) None) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with af'_cfd'(1,2) obtain sa pf where "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and "exists (sa@s') obj'" and "initp_intact (sa@s')" and SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and exfa: "pf \<in> current_files (sa@s')" apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file) apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto) by (frule obj2sobj_file, auto) with af'_cfd'(3) notUkn obtain sb p where SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and soab: "obj2sobj (sb@sa@s') obj' = sobj'" and exsoab: "exists (sb@sa@s') obj'" and intactab: "initp_intact (sb@sa@s')" and nodelab: "no_del_event (sb@sa@s')" apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto) apply (frule obj2sobj_proc, erule exE) by (auto intro:nodel_exists_remains) from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File pf" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all) obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" and tau: "\<tau>=sb@sa@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent) moreover have "rc_grant \<tau> e" using ev tau af'_cfd'(5,6) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps split:if_splits option.splits t_rc_file_type.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t" proof- have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf" using ev tau SPab af'_cfd'(5) by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def split:option.splits intro!:etype_aux_prop3) thus ?thesis using SFab tau ev by (auto simp:obj2sobj.simps split:option.splits if_splits) qed moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd" using ev tau SFab SPab valid ncf_parent by (auto simp:source_dir_simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>] nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps dest:no_del_event_cons_D) qed ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SFile (t, sd) None) \<and> obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, sd) None) obj" using tau ev apply (rule_tac x = "e#sb@sa" in exI) by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto) qed next case (ai'_init i t) hence initi: "i \<in> init_ipcs" using init_ipc_has_type by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'" and nodels': "no_del_event s'"and intacts':"initp_intact s'" and notboth: "not_both_sproc (SIPC t (Some i)) sobj'" and exso': "exists s' obj'" from nodels' initi have exi: "i \<in> current_ipcs s'" by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+) have "obj2sobj s' (IPC i) = SIPC t (Some i)" proof- have "obj2sobj [] (IPC i) = SIPC t (Some i)" using ai'_init initi by (auto simp:obj2sobj.simps) thus ?thesis using vss' exi nodels' initi by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps) qed thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SIPC t (Some i)) \<and> obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC t (Some i)) obj" apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI) by (simp add:vss' sobjs' nodels' intacts' exi exso' del:obj2sobj.simps) qednext case (ai'_cipc r fr pt u srp) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SIPC (default_ipc_create_type r) None) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'" with ai'_cipc(1) notUkn obtain s p where SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and soab: "obj2sobj (s@s') obj' = sobj'" and exsoab: "exists (s@s') obj'" and intactab: "initp_intact (s@s')" and nodelab: "no_del_event (s@s')" apply (drule_tac s'= "s'" and obj' = obj' in all_sobjs_E0, auto) apply (frule obj2sobj_proc, erule exE) by (auto intro:nodel_exists_remains) obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto have valid: "valid (e # \<tau>)" proof- have "os_grant \<tau> e" using ev tau expab by (simp add:ni_notin_curi) moreover have "rc_grant \<tau> e" using ev tau ai'_cipc(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vsab tau by (rule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf) moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using soab tau valid notUkn nodel ev exsoab by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel by (simp add:initp_intact_I_others) moreover have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None" using ev tau SPab nodel nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>] by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps split:option.splits dest:no_del_event_cons_D) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SIPC (default_ipc_create_type r) None) \<and> obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC (default_ipc_create_type r) None) obj" using tau ev by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto) qed next case (ap'_init p r fr t u) hence initp: "p \<in> init_processes" using init_proc_has_role by (simp add:bidirect_in_init_def) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'" and Nodels': "no_del_event s'"and Intacts':"initp_intact s'" and notboth: "not_both_sproc (SProc (r,fr,t,u) (Some p)) sobj'" and exso': "exists s' obj'" from Nodels' initp have exp: "p \<in> current_procs s'" apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted) by (drule not_deleted_imp_exists, simp+) with Intacts' initp ap'_init have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)" by (auto simp:initp_intact_def split:option.splits) thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SProc (r, fr, t, u) (Some p)) \<and> obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (r, fr, t, u) (Some p)) obj" apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI) by (simp add:VSs' SOs' Nodels' Intacts' initp intact_imp_butp exp exso' del:obj2sobj.simps) qednext case (ap'_crole r fr t u srp r') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SProc (r', fr, t, u) srp) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_crole(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'" and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)" by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains) from VSab SPab sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop) with exp VSab SPab have initp: "p \<in> init_processes" by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) obtain e \<tau> where ev: "e = ChangeRole p r'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp) moreover have "rc_grant \<tau> e" using ev tau ap'_crole(3) SPab by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) (SProc (r', fr, t, u) srp)" using butab tau ev valid initp srpeq nodel by (simp add:initp_intact_butp_I_crole) moreover have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False" using Both SOab' notUkn by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc p) = SProc (r', fr, t, u) srp" using SPab tau vs_tau ev valid by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover have "sobj_source_eq_obj (SProc (r', fr, t, u) srp) (Proc p)" using sreq by (case_tac srp, simp+) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SProc (r', fr, t, u) srp) \<and> obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (r', fr, t, u) srp) obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc p" in exI, auto) qednext case (ap'_chown r fr t u srp u' nr) show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SProc (nr,fr,chown_type_aux r nr t,u') srp) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_chown(1,2) obtain s p where VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'" and nodelab: "no_del_event (s@s')" and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)" and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp" and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'" and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)" by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains) from VSab SPab sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop) with exp VSab SPab have initp: "p \<in> init_processes" by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) obtain e \<tau> where ev: "e = ChangeOwner p u'" and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp ap'_chown(3) by (simp) moreover have "rc_grant \<tau> e" using ev tau ap'_chown(5) SPab by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange split:option.splits t_rc_proc_type.splits) (* here is another place of no_limit of clone event assumption *) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) (SProc (nr,fr,chown_type_aux r nr t,u') srp)" using butab tau ev valid initp srpeq nodel by (simp add:initp_intact_butp_I_chown) moreover have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by (auto) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"] by auto moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False" using Both SOab' notUkn by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc p) = SProc (nr,fr,chown_type_aux r nr t,u') srp" using SPab tau vs_tau ev valid ap'_chown(4) by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps split:option.splits) moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover have "sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) (Proc p)" using sreq by (case_tac srp, simp+) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SProc (nr,fr,chown_type_aux r nr t,u') srp) \<and> obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) obj" using ev tau apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI) by (rule_tac x = "Proc p" in exI, auto) qednext case (ap'_exec r fr pt u sp t sd sf r' fr') show ?case proof (rule allI|rule impI|erule conjE)+ fix s' obj' sobj' assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" and Both:"not_both_sproc (SProc (r', fr', exec_type_aux r pt, u) sp) sobj'" and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'" with ap'_exec(3,4) obtain sa f where SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and Exfa: "exists (sa @ s') (File f)" and buta: "initp_intact (sa @ s')" and othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> exists (sa @s') obj' \<and> no_del_event (sa @ s') \<and> sobj_source_eq_obj (SFile (t, sd) sf) (File f)" apply (simp only:not_both_sproc.simps) apply (erule_tac x = s' in allE, erule_tac x = obj' in allE) apply (erule_tac x = sobj' in allE, auto) by (frule obj2sobj_file, auto intro:nodel_exists_remains) with SFa Exfa othersa ap'_exec(1,2) Both notUkn obtain sb p where VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'" and nodelab: "no_del_event (sb@sa@s')" and butab: "initp_intact_but (sb@sa@s') (SProc (r, fr, pt, u) sp)" and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp" and exp:"exists (sb@sa@s') (Proc p)" and exobj':"exists (sb@sa@s') obj'" and sreq: "sobj_source_eq_obj (SProc (r, fr, pt, u) sp) (Proc p)" by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains) from VSab SPab sreq exp have srpeq: "sp = Some p" by (simp add:proc_source_eq_prop) with exp VSab SPab have initp: "p \<in> init_processes" by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits) obtain e \<tau> where ev: "e = Execute p f" and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit) from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" apply (drule_tac obj = "File f" in nodel_imp_un_deleted) by (drule_tac s' = "sb" in not_deleted_imp_exists', auto) from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf" by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all) have valid: "valid (e#\<tau>)" proof- have "os_grant \<tau> e" using ev tau exp by (simp add:exf) moreover have "rc_grant \<tau> e" using ev tau ap'_exec(5) SPab SFab by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps split:if_splits option.splits) ultimately show ?thesis using vs_tau by (erule_tac vs_step, simp+) qed moreover have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover have "initp_intact_but (e#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) sp)" using butab tau ev valid initp srpeq nodel by (simp add:initp_intact_butp_I_exec) moreover have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau by (case_tac obj', simp+) moreover have "obj2sobj (e#\<tau>) obj' = sobj'" proof- have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" using SOab' tau ev valid notUkn nodel exobj' obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"] by (auto simp del:obj2sobj.simps) moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False" using Both SOab' notUkn by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto) ultimately show ?thesis by (case_tac obj', auto) qed moreover have "obj2sobj (e#\<tau>) (Proc p) = SProc (r',fr',exec_type_aux r pt, u) sp" proof- have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps) moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits) ultimately show ?thesis using valid ev ap'_exec(6,7) by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits) qed moreover have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover have "sobj_source_eq_obj (SProc (r',fr',exec_type_aux r pt,u) sp) (Proc p)" using sreq by (case_tac sp, simp+) ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') (SProc (r', fr', exec_type_aux r pt, u) sp) \<and> obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and> exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) sp) obj" using ev tau apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI) by (rule_tac x = "Proc p" in exI, auto) qedqedlemma all_sobjs_E2: "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; not_both_sproc sobj sobj'; no_del_event s'; initp_intact s'\<rbrakk> \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and> sobj_source_eq_obj sobj obj"by (drule all_sobjs_E2_aux, auto)endend