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 split:option.splits)

        apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+)      

        using SP sproc rc ev 

        by (auto intro:ai_cipc)

      with True show ?thesis by simp

    next

      case False 

      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                              split:option.splits t_role.splits )

      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)

    qed

  next

    case (ChangeRole p r')

    assume ev: "e = ChangeRole p r'"

    show ?thesis

    proof (cases "obj = Proc p")

      case True

      from os ev have exp: "exists s (Proc p)" by simp

      then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"

        and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp"

        using prem'[where obj = "Proc p"] vs

        by (auto split:option.splits if_splits simp:obj2sobj.simps 

                  dest:current_proc_has_sproc)

      have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os 

        apply (auto simp:obj2sobj.simps split:option.splits)

        apply (rule ap_crole) using SP sproc rc ev srproc by auto

      with True show ?thesis by simp

    next

      case False 

      hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

        by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                              split:option.splits t_role.splits )

      thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)

    qed

  next

    case (ReadFile p f)

    assume ev: "e = ReadFile p f"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    moreover have "exists s obj" using ev ex_cons

      by (case_tac obj, auto)

    ultimately show ?thesis using prem[where obj = obj] vs by simp

  next

    case (WriteFile p f)

    assume ev: "e = WriteFile p f"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    moreover have "exists s obj" using ev ex_cons

      by (case_tac obj, auto)

    ultimately show ?thesis using prem[where obj = obj] vs by simp

  next

    case (Send p i)

    assume ev: "e = Send p i"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    moreover have "exists s obj" using ev ex_cons

      by (case_tac obj, auto)

    ultimately show ?thesis using prem[where obj = obj] vs by simp

  next

    case (Recv p i)

    assume ev: "e = Recv p i"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    moreover have "exists s obj" using ev ex_cons

      by (case_tac obj, auto)

    ultimately show ?thesis using prem[where obj = obj] vs by simp

  next

    case (Kill p p')

    assume ev: "e = Kill p p'"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    thus ?thesis using prem[where obj = obj] vs ex_cons ev

      by (case_tac obj, auto)

  next

    case (DeleteFile p f')

    assume ev: "e = DeleteFile p f'" 

    have "obj2sobj (e#s) obj = obj2sobj s obj"

    proof-

      have "\<And> f. obj = File f ==> obj2sobj (e#s) (File f) = obj2sobj s (File f)"

        using ev vs os ex_cons vs_cons

        by (auto simp:obj2sobj.simps etype_of_file_delete source_dir_simps

                split:option.splits t_role.splits if_splits

                dest!:current_file_has_etype' current_file_has_sd'

                 dest:source_dir_prop)

      moreover have "\<forall> f. obj \<noteq> File f ==> obj2sobj (e#s) obj = obj2sobj s obj"

        using ev vs_cons ex_cons os vs

        by (case_tac obj, auto simp:obj2sobj.simps split:option.splits)

      ultimately show ?thesis by auto

    qed

    thus ?thesis using prem[where obj = obj] vs ex_cons ev 

      by (case_tac obj, auto)

  next

    case (DeleteIPC p i)

    assume ev: "e = DeleteIPC p i"

    have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs

      by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps 

                            split:option.splits t_role.splits)

    thus ?thesis using prem[where obj = obj] vs ex_cons ev

      by (case_tac obj, auto)

  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)