theory all_sobj_prop
imports Main rc_theory os_rc obj2sobj_prop deleted_prop sound_defs_prop source_prop
begin
context tainting_s_complete begin
lemma 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 vd
proof (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
qed
next
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 ni_init_deled split:option.splits)
apply (rule ai_cipc) using SP sproc rc ev 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 (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 ni_init_deled 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)
qed
qed
declare 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)
qed
lemma 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)
done
end
context 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')
qed
next
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+)
qed
next
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)
qed
next
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)
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)
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 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)
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 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)
qed
next
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)
qed
qed
(* 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')
qed
next
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)
qed
next
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)
qed
next
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)
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)
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)
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)
qed
next
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)
qed
qed
(* 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')
qed
next
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)
qed
next
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)
qed
next
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)
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)
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 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)
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 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)
qed
next
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)
qed
qed
lemma 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)
end
end