1 theory all_sobj_prop

     2 imports Main rc_theory os_rc obj2sobj_prop deleted_prop sound_defs_prop source_prop

     3 begin

     4 

     5 context tainting_s_complete begin

     6 

     7 lemma initf_has_effinitialrole:

     8   "f \<in> init_files ==> \<exists> r. effinitialrole [] f = Some r"

     9 by (rule_tac f = f in file_has_effinitialrole, simp, simp add:vs_nil)

    10 

    11 lemma initf_has_effforcedrole:

    12   "f \<in> init_files ==> \<exists> r. effforcedrole [] f = Some r"

    13 by (rule_tac f = f in file_has_effforcedrole, simp, simp add:vs_nil)

    14 

    15 lemma efffrole_sdir_some:

    16   "sd \<in> init_files ==> \<exists> r. erole_functor init_file_forcedrole InheritUpMixed sd = Some r"

    17 apply (frule_tac s = "[]" in undel_initf_keeps_efrole, simp, simp add:vs_nil)

    18 by (drule initf_has_effforcedrole, simp)

    19 

    20 lemma efffrole_sdir_some':

    21   "erole_functor init_file_forcedrole InheritUpMixed sd = None ==> sd \<notin> init_files"

    22 by (rule notI, auto dest!:efffrole_sdir_some)

    23 

    24 lemma effirole_sdir_some:

    25   "sd \<in> init_files ==> \<exists> r. erole_functor init_file_initialrole UseForcedRole sd = Some r"

    26 apply (frule_tac s = "[]" in undel_initf_keeps_eirole, simp, simp add:vs_nil)

    27 by (drule initf_has_effinitialrole, simp)

    28 

    29 lemma effirole_sdir_some':

    30   "erole_functor init_file_initialrole UseForcedRole sd = None ==> sd \<notin> init_files"

    31 by (rule notI, auto dest:effirole_sdir_some)

    32 

    33 lemma erole_func_irole_simp:

    34   "erole_functor init_file_initialrole UseForcedRole sd = effinitialrole [] sd"

    35 by (simp add:effinitialrole_def)

    36 

    37 lemma erole_func_frole_simp:

    38   "erole_functor init_file_forcedrole InheritUpMixed sd = effforcedrole [] sd"

    39 by (simp add:effforcedrole_def)

    40 

    41 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)"

    42 by (simp add:erole_func_frole_simp, erule effforcedrole_valid)

    43 

    44 lemma init_effinitialrole_valid: "erole_functor init_file_initialrole UseForcedRole sd = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" 

    45 by (simp add:erole_func_irole_simp, erule effinitialrole_valid)

    46 

    47 lemma exec_role_some:

    48   "[|sd \<in> init_files; u \<in> init_users|] ==> \<exists> r'. exec_role_aux r sd u = Some r'"

    49 by (auto simp:exec_role_aux_def split:option.splits t_role.splits 

    50         dest!:effirole_sdir_some' efffrole_sdir_some'

    51         dest:init_effforcedrole_valid init_effinitialrole_valid

    52        intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)

    53 

    54 lemma chown_role_some:

    55   "u \<in> init_users ==> \<exists> r'. chown_role_aux r fr u = Some r'"

    56 by (auto simp:chown_role_aux_def split:option.splits t_role.splits 

    57         dest!:effirole_sdir_some' efffrole_sdir_some'

    58         dest:init_effforcedrole_valid init_effinitialrole_valid

    59        intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)

    60   

    61 declare obj2sobj.simps [simp del]

    62 

    63 lemma all_sobjs_I:

    64   assumes ex: "exists s obj"

    65   and vd: "valid s"

    66   shows "obj2sobj s obj \<in> all_sobjs"

    67 using ex vd

    68 proof (induct s arbitrary:obj)

    69   case Nil

    70   assume ex:"exists [] obj"

    71   show ?case

    72   proof (cases obj)

    73     case (Proc p) assume prem: "obj = Proc p" 

    74     with ex have initp:"p \<in> init_processes" by simp 

    75     from initp obtain r where "init_currentrole p = Some r" 

    76       using init_proc_has_role by (auto simp:bidirect_in_init_def)  

    77     moreover from initp obtain t where "init_process_type p = Some t" 

    78       using init_proc_has_type by (auto simp:bidirect_in_init_def)  

    79     moreover from initp obtain fr where "init_proc_forcedrole p = Some fr" 

    80       using init_proc_has_frole by (auto simp:bidirect_in_init_def)  

    81     moreover from initp obtain u where "init_owner p = Some u" 

    82       using init_proc_has_owner by (auto simp:bidirect_in_init_def)  

    83     ultimately have "obj2sobj [] (Proc p) \<in> all_sobjs" 

    84       using initp by (auto intro!:ap_init simp:obj2sobj.simps)

    85     with prem show ?thesis by simp

    86   next

    87     case (File f) assume prem: "obj = File f"

    88     with ex have initf: "f \<in> init_files" by simp

    89     from initf obtain t where "etype_aux init_file_type_aux f = Some t" 

    90       using init_file_has_etype by auto

    91     moreover from initf have "source_dir [] f = Some f"

    92       by (simp add:source_dir_of_init')

    93     ultimately have "obj2sobj [] (File f) \<in> all_sobjs"

    94       using initf by (auto simp:etype_of_file_def obj2sobj.simps intro!:af_init)

    95     with prem show ?thesis by simp

    96   next

    97     case (IPC i) assume prem: "obj = IPC i"

    98     with ex have initi: "i \<in> init_ipcs" by simp

    99     from initi obtain t where "init_ipc_type i = Some t" 

   100       using init_ipc_has_type by (auto simp:bidirect_in_init_def)

   101     hence "obj2sobj [] (IPC i) \<in> all_sobjs"

   102       using initi by (auto intro!:ai_init simp:obj2sobj.simps) 

   103     with prem show ?thesis by simp

   104   qed

   105 next

   106   case (Cons e s)

   107   assume prem: "\<And> obj. \<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<in> all_sobjs"

   108     and ex_cons: "exists (e # s) obj" and vs_cons: "valid (e # s)"

   109   have vs: "valid s" and rc: "rc_grant s e" and os: "os_grant s e" 

   110     using vs_cons by (auto intro:valid_cons valid_os valid_rc)

   111   from prem and vs have prem': "\<And> obj. exists s obj \<Longrightarrow> obj2sobj s obj \<in> all_sobjs" by simp

   112   show ?case

   113   proof (cases e)

   114     case (ChangeOwner p u)

   115     assume ev: "e = ChangeOwner p u"

   116     show ?thesis

   117     proof (cases "obj = Proc p")

   118       case True 

   119       have curp: "p \<in> current_procs s" and exp: "exists s (Proc p)" using os ev by auto

   120       from curp obtain r fr t u' srp where sp: "obj2sobj s (Proc p) = SProc (r,fr,t,u') (Some srp)" 

   121         using vs apply (drule_tac current_proc_has_sobj, simp) by blast

   122       hence sp_in: "SProc (r,fr,t,u') (Some srp) \<in> all_sobjs" using prem' exp by metis

   123       have comp: "(r, Proc_type t, CHANGE_OWNER) \<in> compatible" using sp ev rc

   124         by (auto simp:obj2sobj.simps split:option.splits)

   125       from os ev have uinit: "u \<in> init_users" by simp

   126       then obtain nr where chown: "chown_role_aux r fr u = Some nr" 

   127         by (auto dest:chown_role_some)

   128       hence nsp_in:"obj2sobj (e#s) (Proc p) = SProc (nr,fr,chown_type_aux r nr t, u) (Some srp)" 

   129         using sp ev os

   130         by (auto split:option.splits t_role.splits 

   131           simp del:currentrole.simps type_of_process.simps

   132           simp add:chown_role_aux_valid chown_type_aux_valid obj2sobj.simps)

   133       thus ?thesis using True ev os rc sp_in sp

   134         by (auto simp:chown comp intro!:ap_chown[where u'=u']) 

   135     next

   136       case False

   137       hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons

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

   139                               split:option.splits t_role.splits)

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

   141     qed

   142   next

   143     case (Clone p p')

   144     assume ev: "e = Clone p p'"

   145     show ?thesis 

   146     proof (cases "obj = Proc p'")

   147       case True

   148       from ev os have exp: "exists s (Proc p)" by (simp add:os_grant.simps)

   149       from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"

   150         and srp: "source_proc s p = Some sp" using vs

   151         apply (simp del:cp2sproc.simps)

   152         by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)

   153       hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs

   154         by (auto split:option.splits simp add:obj2sobj.simps)

   155       have "obj2sobj (e # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)"

   156         using ev sproc srp vs_cons 

   157         by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps)

   158       thus ?thesis using True SP by (simp add:ap_clone)

   159     next

   160       case False

   161       hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons

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

   163                               split:option.splits t_role.splits)

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

   165     qed

   166   next

   167     case (Execute p f)

   168     assume ev: "e = Execute p f"

   169     show ?thesis

   170     proof (cases "obj = Proc p")

   171       case True

   172       from ev os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto

   173       from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"

   174         and srp: "source_proc s p = Some sp" using vs

   175         apply (simp del:cp2sproc.simps)

   176         by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)

   177       hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs

   178         by (auto split:option.splits simp add:obj2sobj.simps)

   179       from exf obtain sd t where srdir: "source_dir s f = Some sd" and 

   180         etype: "etype_of_file s f = Some t" using vs

   181         by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)

   182       then obtain srf where SF: "SFile (t, sd) srf \<in> all_sobjs" 

   183         using exf prem'[where obj = "File f"] vs

   184         by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_file_has_etype)

   185       from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs

   186         by (auto intro:source_dir_in_init owner_in_users split:option.splits)

   187       then obtain nr where "exec_role_aux r sd u = Some nr" by (auto dest:exec_role_some) 

   188       

   189       hence "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons srdir sproc srp 

   190         apply (auto simp:obj2sobj.simps cp2sproc_simps source_proc.simps 

   191                    intro:source_dir_in_init simp del:cp2sproc.simps 

   192                    split:option.splits dest!:efffrole_sdir_some')

   193         apply (rule ap_exec) using SF SP rc ev etype by (auto split:option.splits)

   194       with True show ?thesis by simp

   195     next

   196       case False

   197       hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons

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

   199                               split:option.splits t_role.splits)

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

   201     qed

   202   next

   203     case (CreateFile p f)

   204     assume ev: "e = CreateFile p f"

   205     show ?thesis

   206     proof (cases "obj = File f")

   207       case True

   208       from os ev obtain pf where expf: "exists s (File pf)" and parent:"parent f = Some pf" by auto

   209       from expf obtain pft sd srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs"

   210         and eptype: "etype_of_file s pf = Some pft" and srpf: "source_dir s pf = Some sd"

   211         using prem'[where obj = "File pf"] vs

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

   213                   dest:current_file_has_etype current_file_has_sd)

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

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

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

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

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

   219                   dest:current_proc_has_sproc)

   220       have "obj2sobj (e # s) (File f) \<in> all_sobjs" using ev vs_cons sproc srpf parent os

   221         apply (auto simp:obj2sobj.simps source_dir_simps init_notin_curf_deleted  

   222                    split:option.splits dest!:current_file_has_etype')

   223         apply (case_tac "default_fd_create_type r")

   224         using SF SP rc ev eptype sproc

   225         apply (rule_tac sf = srpf in af_cfd', auto simp:etype_of_file_def etype_aux_prop3) [1]

   226         using SF SP rc ev eptype sproc

   227         apply (rule_tac sf = srpf in af_cfd)

   228         apply (auto simp:etype_of_file_def etype_aux_prop4)

   229         done

   230       with True show ?thesis by simp

   231     next

   232       case False 

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

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

   235                               split:option.splits t_role.splits )

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

   237     qed

   238   next

   239     case (CreateIPC p i)

   240     assume ev: "e = CreateIPC p i"

   241     show ?thesis

   242     proof (cases "obj = IPC i")

   243       case True

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

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

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

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

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

   249                   dest:current_proc_has_sproc)

   250       have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os

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

   252         apply (rule ai_cipc) using SP sproc rc ev by auto

   253       with True show ?thesis by simp

   254     next

   255       case False 

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

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

   258                               split:option.splits t_role.splits )

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

   260     qed

   261   next

   262     case (ChangeRole p r')

   263     assume ev: "e = ChangeRole p r'"

   264     show ?thesis

   265     proof (cases "obj = Proc p")

   266       case True

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

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

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

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

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

   272                   dest:current_proc_has_sproc)

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

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

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

   276       with True show ?thesis by simp

   277     next

   278       case False 

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

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

   281                               split:option.splits t_role.splits )

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

   283     qed

   284   next

   285     case (ReadFile p f)

   286     assume ev: "e = ReadFile p f"

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

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

   289                             split:option.splits t_role.splits)

   290     moreover have "exists s obj" using ev ex_cons

   291       by (case_tac obj, auto)

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

   293   next

   294     case (WriteFile p f)

   295     assume ev: "e = WriteFile p f"

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

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

   298                             split:option.splits t_role.splits)

   299     moreover have "exists s obj" using ev ex_cons

   300       by (case_tac obj, auto)

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

   302   next

   303     case (Send p i)

   304     assume ev: "e = Send p i"

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

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

   307                             split:option.splits t_role.splits)

   308     moreover have "exists s obj" using ev ex_cons

   309       by (case_tac obj, auto)

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

   311   next

   312     case (Recv p i)

   313     assume ev: "e = Recv p i"

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

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

   316                             split:option.splits t_role.splits)

   317     moreover have "exists s obj" using ev ex_cons

   318       by (case_tac obj, auto)

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

   320   next

   321     case (Kill p p')

   322     assume ev: "e = Kill p p'"

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

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

   325                             split:option.splits t_role.splits)

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

   327       by (case_tac obj, auto)

   328   next

   329     case (DeleteFile p f')

   330     assume ev: "e = DeleteFile p f'" 

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

   332     proof-

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

   334         using ev vs os ex_cons vs_cons

   335         by (auto simp:obj2sobj.simps etype_of_file_delete source_dir_simps

   336                 split:option.splits t_role.splits if_splits

   337                 dest!:current_file_has_etype' current_file_has_sd'

   338                  dest:source_dir_prop)

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

   340         using ev vs_cons ex_cons os vs

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

   342       ultimately show ?thesis by auto

   343     qed

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

   345       by (case_tac obj, auto)

   346   next

   347     case (DeleteIPC p i)

   348     assume ev: "e = DeleteIPC p i"

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

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

   351                             split:option.splits t_role.splits)

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

   353       by (case_tac obj, auto)

   354   qed

   355 qed

   356 

   357 declare obj2sobj.simps [simp add]

   358 

   359 lemma seeds_in_all_sobjs: 

   360   assumes seed: "obj \<in> seeds" shows "init_obj2sobj obj \<in> all_sobjs"

   361 proof (cases obj)

   362   case (Proc p)

   363   assume p0: "obj = Proc p" (*?*)

   364   from seed p0 have pinit: "p \<in> init_processes" by (drule_tac seeds_in_init, simp)

   365   from pinit obtain r where "init_currentrole p = Some r" 

   366     using init_proc_has_role by (auto simp:bidirect_in_init_def)

   367   moreover from pinit obtain fr where "init_proc_forcedrole p = Some fr"

   368     using init_proc_has_frole by (auto simp:bidirect_in_init_def)

   369   moreover from pinit obtain pt where "init_process_type p = Some pt"

   370     using init_proc_has_type by (auto simp:bidirect_in_init_def)

   371   moreover from pinit obtain u where "init_owner p = Some u"

   372     using init_proc_has_owner by (auto simp:bidirect_in_init_def)

   373   ultimately show ?thesis using p0 by (auto intro:ap_init)

   374 next

   375   case (File f) 

   376   assume p0: "obj = File f" (*?*)

   377   from seed p0 have finit: "f \<in> init_files" by (drule_tac seeds_in_init, simp)

   378   then obtain t where "etype_aux init_file_type_aux f = Some t"

   379     by (auto dest:init_file_has_etype)

   380   with finit p0 show ?thesis by (auto intro:af_init)

   381 next

   382   case (IPC i)

   383   assume p0: "obj = IPC i" (*?*)

   384   from seed p0 have iinit: "i \<in> init_ipcs" by (drule_tac seeds_in_init, simp)

   385   then obtain t where "init_ipc_type i = Some t" using init_ipc_has_type

   386     by (auto simp:bidirect_in_init_def)

   387   with iinit p0 show ?thesis by (auto intro:ai_init)

   388 qed

   389 

   390 lemma tainted_s_in_all_sobjs:

   391   "sobj \<in> tainted_s \<Longrightarrow> sobj \<in> all_sobjs"

   392 apply (erule tainted_s.induct)

   393 apply (erule seeds_in_all_sobjs)

   394 apply (auto intro:ap_crole ap_exec ap_chown ai_cipc af_cfd af_cfd' ap_clone)

   395 done

   396 

   397 end

   398 

   399 context tainting_s_sound begin

   400 

   401 (*** all_sobjs' equal with all_sobjs in the view of soundness ***)

   402 

   403 lemma all_sobjs'_eq1: "sobj \<in> all_sobjs \<Longrightarrow> sobj \<in> all_sobjs'"

   404 apply (erule all_sobjs.induct)

   405 apply (auto intro:af'_init af'_cfd af'_cfd' ai'_init ai'_cipc ap'_init ap'_crole ap'_exec ap'_chown)

   406 by (simp add:clone_type_aux_def clone_type_unchange)

   407 

   408 lemma all_sobjs'_eq2: "sobj \<in> all_sobjs' \<Longrightarrow> sobj \<in> all_sobjs"

   409 apply (erule all_sobjs'.induct)

   410 by (auto intro:af_init af_cfd af_cfd' ai_init ai_cipc ap_init ap_crole ap_exec ap_chown)

   411 

   412 lemma all_sobjs'_eq: "(sobj \<in> all_sobjs) = (sobj \<in> all_sobjs')"

   413 by (auto intro:iffI all_sobjs'_eq1 all_sobjs'_eq2)

   414 

   415 (************************ all_sobjs Elim Rules ********************)

   416 

   417 declare obj2sobj.simps [simp del]

   418 declare cp2sproc.simps [simp del]

   419 

   420 lemma all_sobjs_E0_aux[rule_format]:

   421   "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))"

   422 proof (induct rule:all_sobjs'.induct)

   423   case (af'_init f t) show ?case

   424   proof (rule allI|rule impI|erule conjE)+

   425     fix s' obj' sobj'

   426     assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"

   427       and nodels': "no_del_event s'"and intacts':"initp_intact s'"

   428       and exso': "exists s' obj'"

   429     from nodels' af'_init(1) have exf: "f \<in> current_files s'" 

   430       by (drule_tac obj = "File f" in nodel_imp_exists, simp+)    

   431     have "obj2sobj s' (File f) = SFile (t, f) (Some f)"

   432     proof-

   433       have "obj2sobj [] (File f) = SFile (t, f) (Some f)"  using af'_init 

   434         by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps

   435                 split:option.splits)

   436       thus ?thesis using vss' exf nodels' af'_init(1) 

   437         by (drule_tac obj2sobj_file_remains_app', auto)

   438     qed

   439     thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   440              exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   441              obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"

   442       apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)

   443       by (simp add:vss' sobjs' nodels' intacts' exf exso')

   444   qed

   445 next

   446   case (af'_cfd t sd srf r fr pt u srp t') 

   447   show ?case 

   448   proof (rule allI|rule impI|erule conjE)+

   449     fix s' obj' sobj'

   450     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   451       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"

   452     with af'_cfd(1,2) obtain sa pf where

   453       "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and

   454       "exists (sa@s') obj'" and "initp_intact (sa@s')" and

   455       SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and

   456       exfa: "pf \<in> current_files (sa@s')" 

   457       apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)

   458       by (frule obj2sobj_file, auto)

   459     with af'_cfd(3,4) notUkn obtain sb p where

   460       SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and

   461       expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and

   462       soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 

   463       exsoab: "exists (sb@sa@s') obj'" and

   464       intactab: "initp_intact (sb@sa@s')" and

   465       nodelab: "no_del_event (sb@sa@s')"

   466       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   467     from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"

   468       apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)

   469       by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)

   470     from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"

   471       by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)

   472     obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 

   473       and tau: "\<tau>=sb@sa@s'" by auto

   474     

   475     have valid: "valid (e # \<tau>)" 

   476     proof-

   477       have "os_grant \<tau> e"

   478         using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)

   479       moreover have "rc_grant \<tau> e" 

   480         using ev tau af'_cfd(5,6,7) SPab SFab

   481         by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps

   482                 split:if_splits option.splits t_rc_file_type.splits)

   483       ultimately show ?thesis using vsab tau

   484         by (rule_tac vs_step, simp+)

   485     qed  moreover

   486     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   487     have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau

   488         by (case_tac obj', simp+)   moreover

   489     have "obj2sobj (e#\<tau>) obj' = sobj'" 

   490     proof-

   491       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   492         using soab tau valid notUkn nodel ev exsoab

   493         by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)

   494       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   495         using soab tau valid notUkn nodel ev exsoab

   496         by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)

   497       moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   498         using soab tau valid notUkn nodel ev exsoab

   499         by (auto simp:obj2sobj.simps cp2sproc_simps 

   500              simp del:cp2sproc.simps split:option.splits)

   501       ultimately show ?thesis by (case_tac obj', auto)

   502     qed  moreover 

   503     have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel

   504       by (simp_all add:initp_intact_I_others)  moreover

   505     have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"

   506     proof-

   507       have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"

   508         using ev tau SFab SPab af'_cfd(5)

   509         by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def

   510           split:option.splits if_splits  intro!:etype_aux_prop4)

   511       moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"

   512         using ev tau SFab SPab valid ncf_parent

   513         by (auto simp:source_dir_simps obj2sobj.simps 

   514                 split:if_splits option.splits)

   515       ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]

   516         nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]

   517         by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)

   518     qed

   519     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   520       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   521       obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "

   522       using tau ev

   523       by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)

   524   qed

   525 next

   526   case (af'_cfd' t sd srf r fr pt u srp)

   527   show ?case 

   528   proof (rule allI|rule impI|erule conjE)+

   529     fix s' obj' sobj'

   530     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   531       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"

   532     with af'_cfd'(1,2) obtain sa pf where

   533       "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and

   534       "exists (sa@s') obj'" and "initp_intact (sa@s')" and

   535       SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and

   536       exfa: "pf \<in> current_files (sa@s')" 

   537       apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)

   538       by (frule obj2sobj_file, auto)

   539     with af'_cfd'(3,4) notUkn obtain sb p where

   540       SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and

   541       expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and

   542       soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 

   543       exsoab: "exists (sb@sa@s') obj'" and

   544       intactab: "initp_intact (sb@sa@s')" and

   545       nodelab: "no_del_event (sb@sa@s')"

   546       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   547     from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"

   548       apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)

   549       by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)

   550     from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"

   551       by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)

   552     obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 

   553       and tau: "\<tau>=sb@sa@s'" by auto

   554     

   555     have valid: "valid (e # \<tau>)" 

   556     proof-

   557       have "os_grant \<tau> e"

   558         using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)

   559       moreover have "rc_grant \<tau> e" 

   560         using ev tau af'_cfd'(5,6) SPab SFab

   561         by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps

   562                 split:if_splits option.splits t_rc_file_type.splits)

   563       ultimately show ?thesis using vsab tau

   564         by (rule_tac vs_step, simp+)

   565     qed  moreover

   566     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   567     have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau

   568         by (case_tac obj', simp+)   moreover

   569     have "obj2sobj (e#\<tau>) obj' = sobj'" 

   570     proof-

   571       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   572         using soab tau valid notUkn nodel ev exsoab

   573         by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)

   574       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   575         using soab tau valid notUkn nodel ev exsoab

   576         by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)

   577       moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   578         using soab tau valid notUkn nodel ev exsoab

   579         by (auto simp:obj2sobj.simps cp2sproc_simps 

   580              simp del:cp2sproc.simps split:option.splits)

   581       ultimately show ?thesis by (case_tac obj', auto)

   582     qed  moreover 

   583     have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel

   584       by (simp add:initp_intact_I_others)  moreover

   585     have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"

   586     proof-

   587       have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"

   588       proof-

   589         have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"

   590           using ev tau SPab af'_cfd'(5) 

   591           by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps

   592             split:option.splits   intro!:etype_aux_prop3)

   593         thus ?thesis using SFab tau ev

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

   595       qed

   596       moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"

   597         using ev tau SFab SPab valid ncf_parent

   598         by (auto simp:source_dir_simps obj2sobj.simps 

   599                 split:if_splits option.splits)

   600       ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]

   601         nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]

   602         by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)

   603     qed

   604     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   605       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   606       obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"

   607       using tau ev

   608       by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)

   609   qed 

   610 next

   611   case (ai'_init i t) 

   612   hence initi: "i \<in> init_ipcs" using init_ipc_has_type

   613     by (simp add:bidirect_in_init_def)

   614   show ?case 

   615   proof (rule allI|rule impI|erule conjE)+

   616     fix s' obj' sobj'

   617     assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"

   618       and nodels': "no_del_event s'"and intacts':"initp_intact s'"

   619       and exso': "exists s' obj'"

   620     from nodels' initi have exi: "i \<in> current_ipcs s'" 

   621       by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)    

   622     have "obj2sobj s' (IPC i) = SIPC t (Some i)"

   623     proof-

   624       have "obj2sobj [] (IPC i) = SIPC t (Some i)"  

   625         using ai'_init initi by (auto simp:obj2sobj.simps)

   626       thus ?thesis using vss' exi nodels' initi 

   627         by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)

   628     qed

   629     thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   630              exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   631              obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj"

   632       apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)

   633       by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps)

   634   qed

   635 next

   636   case (ai'_cipc r fr pt u srp)

   637   show ?case

   638   proof (rule allI|rule impI|erule conjE)+

   639     fix s' obj' sobj'

   640     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   641       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"

   642     with ai'_cipc(1,2) notUkn obtain s p where

   643       SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and

   644       expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and

   645       soab: "obj2sobj (s@s') obj' = sobj'" and 

   646       exsoab: "exists (s@s') obj'" and

   647       intactab: "initp_intact (s@s')" and

   648       nodelab: "no_del_event (s@s')"

   649       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   650     obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto

   651     

   652     have valid: "valid (e # \<tau>)" 

   653     proof-

   654       have "os_grant \<tau> e"

   655         using ev tau expab by (simp)

   656       moreover have "rc_grant \<tau> e" 

   657         using ev tau ai'_cipc(3) SPab

   658         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)

   659       ultimately show ?thesis using vsab tau

   660         by (rule_tac vs_step, simp+)

   661     qed  moreover

   662     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   663     have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau

   664         by (case_tac obj', simp+)   moreover

   665     have "obj2sobj (e#\<tau>) obj' = sobj'" 

   666     proof-

   667       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   668         using soab tau valid notUkn nodel ev exsoab

   669         by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)

   670       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   671         using soab tau valid notUkn nodel ev exsoab

   672         by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)

   673       moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

   674         using soab tau valid notUkn nodel ev exsoab

   675         by (auto simp:obj2sobj.simps cp2sproc_simps 

   676              simp del:cp2sproc.simps split:option.splits)

   677       ultimately show ?thesis by (case_tac obj', auto)

   678     qed  moreover 

   679     have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel

   680       by (simp add:initp_intact_I_others)  moreover

   681     have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"

   682       using ev tau SPab nodel 

   683         nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]

   684       by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps 

   685               split:option.splits  dest:no_del_event_cons_D)

   686     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   687       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   688       obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj"

   689       using tau ev

   690       by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, simp+)

   691   qed 

   692 next

   693   case (ap'_init p r fr t u)

   694   hence initp: "p \<in> init_processes" using init_proc_has_role

   695     by (simp add:bidirect_in_init_def)

   696   show ?case

   697   proof (rule allI|rule impI|erule conjE)+

   698     fix s' obj' sobj'

   699     assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"

   700       and Nodels': "no_del_event s'"and Intacts':"initp_intact s'"

   701       and exso': "exists s' obj'"

   702     from Nodels' initp have exp: "p \<in> current_procs s'" 

   703       apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted)

   704       by (drule not_deleted_imp_exists, simp+)

   705     with Intacts' initp ap'_init have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)"

   706       by (auto simp:initp_intact_def split:option.splits)

   707     thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 

   708              exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>

   709              obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj"

   710       apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI)

   711       by (simp add:VSs' SOs' Nodels' exp exso' initp intact_imp_butp Intacts'

   712                del:obj2sobj.simps)

   713   qed

   714 next

   715   case (ap'_crole r fr t u srp r')

   716   show ?case 

   717   proof (rule allI|rule impI|erule conjE)+

   718     fix s' obj' sobj'

   719     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   720       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"

   721     with ap'_crole(1,2) obtain s p where

   722       VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"

   723       and nodelab: "no_del_event (s@s')"

   724       and intactab: "initp_intact (s@s')"

   725       and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"

   726       and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"

   727       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   728     obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'" 

   729       and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto

   730     hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)

   731 

   732     have valid: "valid (e#\<tau>)" 

   733     proof-

   734       have "os_grant \<tau> e"

   735         using ev tau exp by (simp)

   736       moreover have "rc_grant \<tau> e" 

   737         using ev tau ap'_crole(3) SPab 

   738         by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)

   739       ultimately show ?thesis using vs_tau

   740         by (erule_tac vs_step, simp+)

   741     qed  moreover

   742     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   743     have "initp_intact (e#\<tau>)" using tau ev intactab valid

   744       by (simp add:initp_intact_I_crole)   moreover

   745     have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau

   746       by (case_tac obj', simp+)  moreover

   747     have "obj2sobj (e#\<tau>) obj' = sobj'"

   748     proof-

   749       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   750         using SOab' tau ev valid notUkn nodel exobj'

   751         obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]

   752         by (auto)

   753       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   754         using SOab' tau ev valid notUkn nodel exobj'

   755         obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]

   756         by auto

   757       moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"

   758         apply (case_tac "p' = new_proc (s @ s')") 

   759         using vs_tau exobj'ab tau

   760         apply (simp, drule_tac valid_os, simp add:np_notin_curp)

   761         using tau ev SOab' valid notUkn vs_tau

   762         by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits)

   763       ultimately show ?thesis by (case_tac obj', auto)

   764     qed  moreover 

   765     have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp"

   766       using SPab tau vs_tau ev valid

   767       by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps

   768               split:option.splits)  moreover

   769     have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp  

   770     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 

   771       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 

   772       obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj"

   773       using ev tau

   774       apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)

   775       by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)

   776   qed

   777 next

   778   case (ap'_chown r fr t u srp u' nr)

   779   show ?case 

   780   proof (rule allI|rule impI|erule conjE)+

   781     fix s' obj' sobj'

   782     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   783       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"

   784     with ap'_chown(1,2) obtain s p where

   785       VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"

   786       and nodelab: "no_del_event (s@s')" and intactab: "initp_intact (s@s')"

   787       and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"

   788       and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"

   789       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   790     obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'" 

   791       and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto

   792     hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)

   793 

   794     have valid: "valid (e#\<tau>)" 

   795     proof-

   796       have "os_grant \<tau> e"

   797         using ev tau exp ap'_chown(3) by (simp)

   798       moreover have "rc_grant \<tau> e" 

   799         using ev tau ap'_chown(5) SPab 

   800         by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange

   801                 split:option.splits t_rc_proc_type.splits)

   802           (* here is another place of no_limit of clone event assumption *)

   803       ultimately show ?thesis using vs_tau

   804         by (erule_tac vs_step, simp+)

   805     qed  moreover

   806     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   807     have "initp_intact (e#\<tau>)" using intactab tau ev valid 

   808       by (simp add:initp_intact_I_chown)  moreover

   809     have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau

   810       by (case_tac obj', simp+)  moreover

   811     have "obj2sobj (e#\<tau>) obj' = sobj'"

   812     proof-

   813       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   814         using SOab' tau ev valid notUkn nodel exobj'

   815         obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]

   816         by (auto)

   817       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   818         using SOab' tau ev valid notUkn nodel exobj'

   819         obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]

   820         by auto

   821       moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"

   822         apply (case_tac "p' = new_proc (s @ s')") 

   823         using vs_tau exobj'ab tau

   824         apply (simp, drule_tac valid_os, simp add:np_notin_curp)

   825         using tau ev SOab' valid notUkn vs_tau 

   826         by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)

   827       ultimately show ?thesis by (case_tac obj', auto)

   828     qed  moreover 

   829     have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = 

   830           SProc (nr,fr,chown_type_aux r nr t,u') srp"

   831       using SPab tau vs_tau ev valid ap'_chown(4)

   832       by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps

   833               split:option.splits)  moreover

   834     have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp   moreover 

   835     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> 

   836       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 

   837       obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>

   838       exists (s @ s') obj"

   839       using ev tau

   840       apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)

   841       by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)

   842   qed

   843 next

   844   case (ap'_exec r fr pt u sp t sd sf r' fr')

   845   show ?case

   846   proof (rule allI|rule impI|erule conjE)+

   847     fix s' obj' sobj'

   848     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   849       and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"

   850     with ap'_exec(3,4) obtain sa f where

   851       SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and

   852       Exfa: "exists (sa @ s') (File f)" and 

   853       butsa: "initp_intact (sa @ s')" and

   854       othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> 

   855                exists (sa @s') obj' \<and> no_del_event (sa @ s')" 

   856       by (blast dest:obj2sobj_file intro:nodel_exists_remains)

   857     with ap'_exec(1,2) notUkn obtain sb p where

   858       VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"

   859       and nodelab: "no_del_event (sb@sa@s')"

   860       and intactab: "initp_intact (sb@sa@s')"

   861       and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"

   862       and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'"

   863       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   864     obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f" 

   865       and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto

   866     hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)

   867     from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')" 

   868       apply (drule_tac obj = "File f" in nodel_imp_un_deleted)

   869       by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)

   870     from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"

   871       by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)

   872 

   873     have valid: "valid (e#\<tau>)" 

   874     proof-

   875       have "os_grant \<tau> e"

   876         using ev tau exp by (simp add:exf)

   877       moreover have "rc_grant \<tau> e" 

   878         using ev tau ap'_exec(5) SPab SFab

   879         by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps

   880                 split:if_splits option.splits)

   881       ultimately show ?thesis using vs_tau

   882         by (erule_tac vs_step, simp+)

   883     qed  moreover

   884     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

   885     have "initp_intact (e#\<tau>)" using tau ev intactab valid

   886       by (simp add:initp_intact_I_exec)  moreover

   887     have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau

   888       by (case_tac obj', simp+) moreover

   889     have "obj2sobj (e#\<tau>) obj' = sobj'"

   890     proof-

   891       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   892         using SOab' tau ev valid notUkn nodel exobj'

   893         obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]

   894         by (auto simp del:obj2sobj.simps)

   895       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

   896         using SOab' tau ev valid notUkn nodel exobj'

   897         obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]

   898         by (auto simp del:obj2sobj.simps)

   899       moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"

   900         apply (case_tac "p' = new_proc (sb @ sa @ s')") 

   901         using vs_tau exobj'ab tau

   902         apply (simp, drule_tac valid_os, simp add:np_notin_curp)

   903         using tau ev SOab' valid notUkn vs_tau 

   904         by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)

   905       ultimately show ?thesis by (case_tac obj', auto)

   906     qed  moreover 

   907     have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) = 

   908           SProc (r',fr',exec_type_aux r pt, u) sp"

   909     proof-

   910       have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau

   911         by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)

   912       hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau

   913       by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange 

   914               split:option.splits)

   915       moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau 

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

   917       ultimately show ?thesis using valid ev ap'_exec(6,7) 

   918         by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)

   919     qed 

   920     ultimately 

   921     show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   922       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 

   923       obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>

   924       exists (s @ s') obj"

   925       using ev tau

   926       apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)

   927       by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto)

   928   qed

   929 qed

   930 

   931 (* this is for ts2t createfile case ... *)

   932 lemma all_sobjs_E0:

   933   "\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown; 

   934     no_del_event s'; initp_intact s'\<rbrakk>

   935    \<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>

   936                 no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> 

   937                 obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"

   938 by (drule all_sobjs_E0_aux, auto)

   939 

   940 lemma all_sobjs_E1_aux[rule_format]:

   941   "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))"

   942 proof (induct rule:all_sobjs'.induct)

   943   case (af'_init f t) show ?case

   944   proof (rule allI|rule impI|erule conjE)+

   945     fix s' obj' sobj'

   946     assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"

   947       and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'"

   948       and exso': "exists s' obj'"

   949     from nodels' af'_init(1) have exf: "f \<in> current_files s'" 

   950       by (drule_tac obj = "File f" in nodel_imp_exists, simp+)    

   951     have "obj2sobj s' (File f) = SFile (t, f) (Some f)"

   952     proof-

   953       have "obj2sobj [] (File f) = SFile (t, f) (Some f)"  using af'_init 

   954         by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps

   955                 split:option.splits)

   956       thus ?thesis using vss' exf nodels' af'_init(1) 

   957         by (drule_tac obj2sobj_file_remains_app', auto)

   958     qed

   959     thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

   960              exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>

   961              obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"

   962       apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)

   963       by (simp add:vss' sobjs' nodels' intacts' exf exso')

   964   qed

   965 next

   966   case (af'_cfd t sd srf r fr pt u srp t') 

   967   show ?case 

   968   proof (rule allI|rule impI|erule conjE)+

   969     fix s' obj' sobj'

   970     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

   971       and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" 

   972       and exobj':"exists s' obj'"

   973     with af'_cfd(1,2) obtain sa pf where

   974       "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and

   975       "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and

   976       SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and

   977       exfa: "pf \<in> current_files (sa@s')" 

   978       apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)

   979       by (frule obj2sobj_file, auto)

   980     with af'_cfd(3,4) notUkn obtain sb p where

   981       SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and

   982       expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and

   983       soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 

   984       exsoab: "exists (sb@sa@s') obj'" and

   985       intactab: "initp_intact_but (sb@sa@s') sobj'" and

   986       nodelab: "no_del_event (sb@sa@s')"

   987       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

   988     from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"

   989       apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)

   990       by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)

   991     from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"

   992       by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)

   993     obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 

   994       and tau: "\<tau>=sb@sa@s'" by auto

   995     

   996     have valid: "valid (e # \<tau>)" 

   997     proof-

   998       have "os_grant \<tau> e"

   999         using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)

  1000       moreover have "rc_grant \<tau> e" 

  1001         using ev tau af'_cfd(5,6,7) SPab SFab

  1002         by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps

  1003                 split:if_splits option.splits t_rc_file_type.splits)

  1004       ultimately show ?thesis using vsab tau

  1005         by (rule_tac vs_step, simp+)

  1006     qed  moreover

  1007     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

  1008     have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau

  1009         by (case_tac obj', simp+)   moreover

  1010     have "obj2sobj (e#\<tau>) obj' = sobj'" 

  1011     proof-

  1012       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

  1013         using soab tau valid notUkn nodel ev exsoab

  1014         by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)

  1015       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

  1016         using soab tau valid notUkn nodel ev exsoab

  1017         by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)

  1018       moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

  1019         using soab tau valid notUkn nodel ev exsoab

  1020         by (auto simp:obj2sobj.simps cp2sproc_simps' 

  1021              simp del:cp2sproc.simps split:option.splits)

  1022       ultimately show ?thesis by (case_tac obj', auto)

  1023     qed  moreover 

  1024     have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"

  1025     proof-

  1026       have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"

  1027         using ev tau SFab SPab af'_cfd(5)

  1028         by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def

  1029           split:option.splits if_splits  intro!:etype_aux_prop4)

  1030       moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"

  1031         using ev tau SFab SPab valid ncf_parent

  1032         by (auto simp:source_dir_simps obj2sobj.simps 

  1033                 split:if_splits option.splits)

  1034       ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]

  1035         nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]

  1036         by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)

  1037     qed  moreover

  1038     have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel

  1039         apply (case_tac sobj', case_tac option)

  1040         by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)  

  1041     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

  1042       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>

  1043       obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "

  1044       using tau ev

  1045       apply (rule_tac x = "e#sb@sa" in exI)

  1046       by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)

  1047   qed

  1048 next

  1049   case (af'_cfd' t sd srf r fr pt u srp)

  1050   show ?case 

  1051   proof (rule allI|rule impI|erule conjE)+

  1052     fix s' obj' sobj'

  1053     assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'" 

  1054       and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" 

  1055       and exobj':"exists s' obj'"

  1056     with af'_cfd'(1,2) obtain sa pf where

  1057       "valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and

  1058       "exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and

  1059       SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and

  1060       exfa: "pf \<in> current_files (sa@s')" 

  1061       apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)

  1062       by (frule obj2sobj_file, auto)

  1063     with af'_cfd'(3,4) notUkn obtain sb p where

  1064       SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and

  1065       expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and

  1066       soab: "obj2sobj (sb@sa@s') obj' = sobj'" and 

  1067       exsoab: "exists (sb@sa@s') obj'" and

  1068       intactab: "initp_intact_but (sb@sa@s') sobj'" and

  1069       nodelab: "no_del_event (sb@sa@s')"

  1070       by (blast dest:obj2sobj_proc intro:nodel_exists_remains)

  1071     from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"

  1072       apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)

  1073       by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)

  1074     from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"

  1075       by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)

  1076     obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)" 

  1077       and tau: "\<tau>=sb@sa@s'" by auto

  1078     

  1079     have valid: "valid (e # \<tau>)" 

  1080     proof-

  1081       have "os_grant \<tau> e"

  1082         using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)

  1083       moreover have "rc_grant \<tau> e" 

  1084         using ev tau af'_cfd'(5,6) SPab SFab

  1085         by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps

  1086                 split:if_splits option.splits t_rc_file_type.splits)

  1087       ultimately show ?thesis using vsab tau

  1088         by (rule_tac vs_step, simp+)

  1089     qed  moreover

  1090     have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp  moreover

  1091     have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau

  1092         by (case_tac obj', simp+)   moreover

  1093     have "obj2sobj (e#\<tau>) obj' = sobj'" 

  1094     proof-

  1095       have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'" 

  1096         using soab tau valid notUkn nodel ev exsoab

  1097         by (auto  intro!:obj2sobj_file_remains' simp:ncf_notin_curf)

  1098       moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

  1099         using soab tau valid notUkn nodel ev exsoab

  1100         by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)

  1101       moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"  

  1102         using soab tau valid notUkn nodel ev exsoab

  1103         by (auto simp:obj2sobj.simps cp2sproc_simps' 

  1104              simp del:cp2sproc.simps split:option.splits)

  1105       ultimately show ?thesis by (case_tac obj', auto)

  1106     qed  moreover 

  1107     have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"

  1108     proof-

  1109       have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"

  1110       proof-

  1111         have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"

  1112           using ev tau SPab af'_cfd'(5) 

  1113           by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def

  1114             split:option.splits   intro!:etype_aux_prop3)

  1115         thus ?thesis using SFab tau ev

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

  1117       qed

  1118       moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"

  1119         using ev tau SFab SPab valid ncf_parent

  1120         by (auto simp:source_dir_simps obj2sobj.simps 

  1121                 split:if_splits option.splits)

  1122       ultimately show ?thesis  using nodel ncf_notin_curf[where s = \<tau>]

  1123         nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]

  1124         by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)

  1125     qed  moreover

  1126     have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel

  1127         apply (case_tac sobj', case_tac option)

  1128         by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)  

  1129     ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>

  1130       exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>

  1131       obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"

  1132       using tau ev

  1133       apply (rule_tac x = "e#sb@sa" in exI)

  1134       by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)

  1135   qed