diff -r b992684e9ff6 -r dcde836219bc obj2sobj_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/obj2sobj_prop.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,674 @@
+theory obj2sobj_prop 
+imports Main rc_theory os_rc deleted_prop
+begin
+
+context tainting_s_complete begin
+
+(** file 2 sfile   **)
+
+lemma init_son_deleted_D:
+  "\<lbrakk>deleted (File pf) s; f # pf \<in> init_files; valid s\<rbrakk> \<Longrightarrow> deleted (File (f # pf)) s"
+apply (induct s, simp)
+by (frule valid_cons, frule valid_os, case_tac a, auto dest:init_notin_curf_deleted)
+
+lemma init_parent_undeleted_I:
+  "\<lbrakk>\<not> deleted (File (f # pf)) s; f # pf \<in> init_files; valid s\<rbrakk> \<Longrightarrow> \<not> deleted (File pf) s"
+by (rule notI, simp add:init_son_deleted_D)
+
+lemma source_dir_in_init:
+  "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+by (induct f, auto split:if_splits)
+
+lemma source_dir_of_init: "\<lbrakk>source_dir [] f = Some sd; f \<in> init_files\<rbrakk> \<Longrightarrow> f = sd"
+by (induct f, auto)
+
+lemma source_dir_of_init': "f \<in> init_files \<Longrightarrow> source_dir [] f = Some f"
+by (induct f, auto)
+
+lemma init_not_curf_imp_deleted:
+  "\<lbrakk>f \<in> init_files; f \<notin> current_files s; valid s\<rbrakk> \<Longrightarrow> deleted (File f) s"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os, case_tac a, auto)
+done
+
+lemma source_dir_of_init'': 
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> source_dir s f = Some f"
+by (induct f, auto)
+
+
+lemma source_dir_createf:
+  "valid (CreateFile p (f#pf) # s) \<Longrightarrow> 
+  source_dir (CreateFile p (f#pf) # s) = (source_dir s) ((f#pf)  := source_dir s pf)"
+apply (frule valid_os, frule valid_cons)
+apply (rule ext, induct_tac x)
+apply (auto dest:init_not_curf_imp_deleted)
+done
+
+lemma source_dir_createf':
+  "valid (CreateFile p f # s) \<Longrightarrow> 
+  source_dir (CreateFile p f # s) = (source_dir s) (f := (case (parent f) of
+                                                            Some pf \<Rightarrow> source_dir s pf
+                                                          | _       \<Rightarrow> None))"
+apply (frule valid_os, case_tac f, simp+)
+apply (drule source_dir_createf, auto)
+done
+
+lemma source_dir_other:
+  "\<lbrakk>valid (e # s); \<forall> p f. e \<noteq> CreateFile p f; \<forall> p f. e \<noteq> DeleteFile p f\<rbrakk>
+   \<Longrightarrow> source_dir (e#s) = source_dir s"
+apply (rule ext, induct_tac x, simp)
+apply (auto dest:not_deleted_cons_D)
+apply (case_tac [!] e, auto)
+done
+
+lemma source_dir_deletef:
+  "valid (DeleteFile p f # s) \<Longrightarrow> source_dir (DeleteFile p f # s) f' =  
+     (if (source_dir s f') = Some f then parent f else (source_dir s f'))"
+apply (frule valid_os, frule valid_cons)
+apply (case_tac "f \<in> init_files")
+apply (induct_tac f', simp)
+apply (auto dest!:init_parent_undeleted_I intro:parent_file_in_init'
+            intro!: source_dir_of_init'')[1]
+apply (induct_tac f', auto)
+done
+
+lemma source_dir_deletef':
+  "valid (DeleteFile p f # s) \<Longrightarrow> source_dir (DeleteFile p f # s) = (\<lambda> f'.   
+     (if (source_dir s f') = Some f then parent f else (source_dir s f')) )"
+by (auto dest:source_dir_deletef)
+
+lemmas source_dir_simps = source_dir_of_init' source_dir_of_init'' source_dir_createf' 
+  source_dir_deletef' source_dir_other
+
+declare source_dir.simps [simp del]
+
+lemma source_dir_is_ancient:
+  "source_dir s f = Some sd ==> sd \<preceq> f"
+apply (induct f)
+by (auto simp:source_dir.simps no_junior_def split:if_splits)
+
+lemma no_junior_trans: "\<lbrakk>f \<preceq> f'; f' \<preceq> f''\<rbrakk> \<Longrightarrow> f \<preceq> f''"
+by (auto elim:no_juniorE)
+
+lemma ancient_has_parent:
+  "[| f \<preceq> f'; f \<noteq> f'|] ==> \<exists> sonf. parent sonf = Some f \<and> sonf \<preceq> f' "
+apply (induct f')
+apply (simp add:no_junior_def)
+apply (case_tac "f = f'")
+apply (rule_tac x = "a # f'" in exI, simp add:no_junior_def)
+apply (frule no_junior_noteq, simp)
+apply clarsimp
+apply (rule_tac x = sonf in exI, simp add:no_junior_trans)
+done
+
+lemma source_dir_prop:
+  "[|\<forall>fn. fn # f' \<notin> current_files s; source_dir s f = Some f'; f \<in> current_files s; valid s|]
+  ==> f = f'"
+  apply (drule source_dir_is_ancient)
+  apply (case_tac "f = f'", simp)
+  apply (drule ancient_has_parent, simp, clarsimp)
+  apply (drule_tac ancient_file_in_current, simp+)
+  apply (case_tac sonf, auto)
+  done
+
+lemma current_file_has_sd:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sd. source_dir s f = Some sd"
+apply (induct s arbitrary:f, simp add:source_dir_of_init')
+apply (frule valid_cons, frule valid_os, case_tac a, auto simp:source_dir_simps)
+apply (case_tac list, simp)
+apply (rule_tac f = f in cannot_del_root, simp+)
+done
+
+lemma current_file_has_sd':
+  "\<lbrakk>source_dir s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:current_file_has_sd)
+
+lemma current_file_has_sfile:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> et sd. cf2sfile s f = Some (et, sd)"
+apply (frule current_file_has_sd, simp+)
+apply (frule current_file_has_etype, auto)
+done
+
+lemma current_file_has_sfile':
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
+by (auto dest:current_file_has_sfile)
+  
+(*
+lemma not_deleted_sf_remains:
+  "\<lbrakk>f \<in> current_files s; \<not> deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> "
+*)
+
+lemma current_proc_has_sproc:
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r fr pt u. cp2sproc s p = Some (r, fr, pt, u)"
+apply (frule current_proc_has_role, simp+)
+apply (frule current_proc_has_type, simp)
+apply (frule current_proc_has_forcedrole, simp)
+apply (frule current_proc_has_owner, auto)
+done
+
+lemma current_proc_has_sproc':
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"
+by (auto dest!:current_proc_has_sproc)
+
+lemma current_ipc_has_sipc: 
+  "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. ci2sipc s i = Some t"
+by (drule current_ipc_has_type, auto)
+
+lemma init_file_has_sobj:
+  "f \<in> init_files \<Longrightarrow> \<exists> t sd. init_obj2sobj (File f) = SFile (t, sd) (Some f)"
+by (frule init_file_has_etype, clarsimp)
+
+lemma init_proc_has_sobj:
+  assumes pinit:"p \<in> init_processes"
+  shows "\<exists> r fr pt u. init_obj2sobj (Proc p) = SProc (r, fr, pt, u) (Some p)"
+proof -
+  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 by auto 
+qed
+
+lemma init_ipc_has_sobj:
+  "i \<in> init_ipcs \<Longrightarrow> \<exists> t. init_obj2sobj (IPC i) = SIPC t (Some i)"
+using init_ipc_has_type
+by (auto simp:bidirect_in_init_def)
+
+lemma init_obj_has_sobj:
+  "exists [] obj \<Longrightarrow> init_obj2sobj obj \<noteq> Unknown"
+apply (case_tac obj)
+apply (simp_all only:exists.simps current_procs.simps current_ipcs.simps current_files.simps) 
+apply (auto dest!:init_proc_has_sobj init_file_has_sobj init_ipc_has_sobj)
+done
+
+lemma exists_obj_has_sobj:
+  "\<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<noteq> Unknown"
+apply (case_tac obj)
+apply (auto dest!:current_ipc_has_sipc current_proc_has_sproc' current_file_has_sfile' 
+            split:option.splits)
+done
+
+lemma current_proc_has_srp:
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> srp. source_proc s p = Some srp"
+apply (induct s arbitrary:p, simp)
+by (frule valid_cons, frule valid_os, case_tac a, auto)
+
+lemma current_proc_has_sobj:
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r fr t u srp. obj2sobj s (Proc p) = SProc (r,fr,t,u) (Some srp)"
+apply (frule current_proc_has_sproc')
+apply (auto dest:current_proc_has_srp)
+done
+
+lemma current_file_has_sobj:
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> t sd srf. obj2sobj s (File f) = SFile (t, sd) srf"
+by (auto dest:current_file_has_sfile)
+
+lemma current_ipc_has_sobj:
+  "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t sri. obj2sobj s (IPC i) = SIPC t sri"
+by (auto dest:current_ipc_has_sipc)
+
+lemma sobj_has_proc_role:
+  "obj2sobj s (Proc p) = SProc (r, fr, t, u) srp \<Longrightarrow> currentrole s p = Some r"
+by (auto split:option.splits)
+
+lemma chown_role_aux_valid:
+  "\<lbrakk>currentrole s p = Some r; proc_forcedrole s p = Some fr\<rbrakk>
+  \<Longrightarrow> chown_role_aux r fr u = currentrole (ChangeOwner p u # s) p"
+by (auto split:t_role.splits simp:chown_role_aux_def dest:proc_forcedrole_valid)
+
+lemma chown_role_aux_valid':
+  "cp2sproc s p = Some (r, fr, t, u') \<Longrightarrow> chown_role_aux r fr u = currentrole (ChangeOwner p u # s) p"
+by (rule chown_role_aux_valid, auto split:option.splits)
+
+lemma chown_type_aux_valid:
+  "\<lbrakk>currentrole s p = Some r; currentrole (ChangeOwner p u # s) p = Some nr; type_of_process s p = Some t\<rbrakk>
+  \<Longrightarrow> type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)" 
+apply (auto split:option.splits t_rc_proc_type.splits 
+             dest:default_process_create_type_valid
+             simp:chown_type_aux_def pot_def pct_def)
+done
+
+lemma chown_type_aux_valid':
+  "\<lbrakk>cp2sproc s p = Some (r, fr, t, u'); currentrole (ChangeOwner p u # s) p = Some nr\<rbrakk> 
+   \<Longrightarrow> type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)"
+by (rule chown_type_aux_valid, auto split:option.splits)
+
+lemma exec_type_aux_valid:
+  "\<lbrakk>currentrole s p = Some r; type_of_process s p = Some t\<rbrakk>
+  \<Longrightarrow> type_of_process (Execute p f # s) p = Some (exec_type_aux r t)" 
+apply (auto split:option.splits t_rc_proc_type.splits 
+             dest:default_process_execute_type_valid
+             simp:exec_type_aux_def pet_def)
+done
+
+lemma exec_type_aux_valid':
+  "cp2sproc s p = Some (r, fr, t, u') \<Longrightarrow> type_of_process (Execute p f # s) p = Some (exec_type_aux r t)" 
+by (rule exec_type_aux_valid, auto split:option.splits)
+
+lemma non_initf_frole_inherit:
+  "\<lbrakk>f \<notin> init_files; f \<noteq> []\<rbrakk> \<Longrightarrow> forcedrole s f = Some InheritParentRole"
+apply (induct s) defer
+apply (case_tac a, auto) 
+apply (induct f, auto split:option.splits dest:init_frole_has_file)
+done
+
+lemma non_initf_irole_inherit:
+  "\<lbrakk>f \<notin> init_files; f \<noteq> []\<rbrakk> \<Longrightarrow> initialrole s f = Some InheritParentRole"
+apply (induct s) defer
+apply (case_tac a, auto) 
+apply (induct f, auto split:option.splits dest:init_irole_has_file)
+done
+
+lemma deleted_file_frole_inherit:
+  "\<lbrakk>deleted (File f) s; f \<in> current_files s\<rbrakk> \<Longrightarrow> forcedrole s f = Some InheritParentRole"
+apply (induct s, simp)
+apply (case_tac a, auto) 
+done
+
+lemma deleted_file_irole_inherit:
+  "\<lbrakk>deleted (File f) s; f \<in> current_files s\<rbrakk> \<Longrightarrow> initialrole s f = Some InheritParentRole"
+apply (induct s, simp)
+apply (case_tac a, auto) 
+done
+
+lemma sd_deter_efrole:
+  "\<lbrakk>source_dir s f = Some sd; valid s; f \<in> current_files s\<rbrakk> 
+  \<Longrightarrow> effforcedrole s f = effforcedrole s sd"
+apply (induct f)
+apply (drule source_dir_is_ancient, simp add:no_junior_def)
+apply (simp add:source_dir.simps split:if_splits)
+apply (frule parent_file_in_current', simp)
+apply (case_tac "a # f \<in> init_files", simp)
+apply (drule_tac deleted_file_frole_inherit, simp, simp add:effforcedrole_def)
+apply (drule_tac s = s in non_initf_frole_inherit, simp, simp add:effforcedrole_def)
+done
+
+lemma sd_deter_eirole:
+  "\<lbrakk>source_dir s f = Some sd; valid s; f \<in> current_files s\<rbrakk> 
+  \<Longrightarrow> effinitialrole s f = effinitialrole s sd"
+apply (induct f)
+apply (drule source_dir_is_ancient, simp add:no_junior_def)
+apply (simp add:source_dir.simps split:if_splits)
+apply (frule parent_file_in_current', simp)
+apply (case_tac "a # f \<in> init_files", simp)
+apply (drule_tac deleted_file_irole_inherit, simp, simp add:effinitialrole_def)
+apply (drule_tac s = s in non_initf_irole_inherit, simp, simp add:effinitialrole_def)
+done
+
+lemma undel_initf_keeps_frole:
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>
+   \<Longrightarrow> forcedrole s f = init_file_forcedrole f"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto dest:init_notin_curf_deleted)
+done
+
+lemma undel_initf_keeps_efrole:
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>
+   \<Longrightarrow> effforcedrole s f = erole_functor init_file_forcedrole InheritUpMixed f"
+apply (induct f)
+apply (drule undel_initf_keeps_frole, simp, simp)
+apply (simp add:effforcedrole_def)
+apply (frule parent_file_in_init', frule init_parent_undeleted_I, simp+)
+apply (drule undel_initf_keeps_frole, simp, simp)
+apply (simp add:effforcedrole_def)
+done
+
+lemma undel_initf_keeps_irole:
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>
+   \<Longrightarrow> initialrole s f = init_file_initialrole f"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto dest:init_notin_curf_deleted)
+done
+
+lemma undel_initf_keeps_eirole:
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>
+   \<Longrightarrow> effinitialrole s f = erole_functor init_file_initialrole UseForcedRole f"
+apply (induct f)
+apply (drule undel_initf_keeps_irole, simp, simp)
+apply (simp add:effinitialrole_def)
+apply (frule parent_file_in_init', frule init_parent_undeleted_I, simp+)
+apply (drule undel_initf_keeps_irole, simp, simp)
+apply (simp add:effinitialrole_def)
+done
+
+lemma source_dir_not_deleted:
+  "source_dir s f = Some sd \<Longrightarrow> \<not> deleted (File sd) s"
+by (induct f, auto simp:source_dir.simps split:if_splits)
+
+lemma exec_role_aux_valid:
+  "\<lbrakk>currentrole s p = Some r; source_dir s f = Some sd; owner s p = Some u; 
+  f \<in> current_files s; valid s\<rbrakk>
+  \<Longrightarrow> exec_role_aux r sd u = currentrole (Execute p f # s) p"
+apply (frule sd_deter_eirole, simp+, frule sd_deter_efrole, simp+)
+apply (frule source_dir_in_init, drule source_dir_not_deleted)
+apply (simp add:undel_initf_keeps_eirole undel_initf_keeps_efrole)
+apply (frule file_has_effinitialrole, simp, frule file_has_effforcedrole, simp)
+apply (auto split:option.splits t_role.splits simp:map_comp_def exec_role_aux_def
+             dest:effforcedrole_valid effinitialrole_valid)
+done
+
+lemma exec_role_aux_valid':
+  "\<lbrakk>cp2sproc s p = Some (r, fr, t, u); source_dir s f = Some sd; f \<in> current_files s; valid s\<rbrakk>
+  \<Longrightarrow> exec_role_aux r sd u = currentrole (Execute p f # s) p"
+by (rule exec_role_aux_valid, auto split:option.splits)
+
+lemma cp2sproc_nil_init:
+  "init_obj2sobj (Proc p) = (case (cp2sproc [] p) of 
+                               Some sp \<Rightarrow> SProc sp (Some p)
+                             | _       \<Rightarrow> Unknown)"
+by (auto split:option.splits)
+
+lemma cf2sfile_nil_init:
+  "init_obj2sobj (File f) = (case (cf2sfile [] f) of 
+                               Some sf \<Rightarrow> SFile sf (Some f)
+                             | _       \<Rightarrow> Unknown)"
+apply (auto split:option.splits simp:etype_of_file_def)
+apply (case_tac "f \<in> init_files", simp add:source_dir_of_init')
+apply (induct f, simp+)
+apply (case_tac "f \<in> init_files", simp add:source_dir_of_init')
+apply (induct f, simp+)
+done
+
+lemma ci2sipc_nil_init:
+  "init_obj2sobj (IPC i) = (case (ci2sipc [] i) of 
+                              Some si \<Rightarrow> SIPC si (Some i)
+                            | _       \<Rightarrow> Unknown)"
+by simp
+
+lemma obj2sobj_nil_init:
+  "exists [] obj \<Longrightarrow> obj2sobj [] obj = init_obj2sobj obj" 
+apply (case_tac obj) 
+apply (auto simp:cf2sfile_nil_init cp2sproc_nil_init ci2sipc_nil_init 
+                 source_dir_of_init' etype_of_file_def
+           split:if_splits option.splits)
+done
+
+(**** cp2sproc simpset ****)
+
+lemma current_proc_has_role':
+  "\<lbrakk>currentrole s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+by (rule notI, auto dest:current_proc_has_role)
+
+lemma cp2sproc_chown:
+  assumes vs: "valid (ChangeOwner p u # s)"
+  shows "cp2sproc (ChangeOwner p u # s) = (cp2sproc s) 
+     (p := (case (cp2sproc s p) of
+              Some (r,fr,pt,u') \<Rightarrow> (case (chown_role_aux r fr u) of 
+                                      Some nr \<Rightarrow> Some (nr,fr,chown_type_aux r nr pt,u)
+                                    | _       \<Rightarrow> None)
+            | _                 \<Rightarrow> None)
+      )" (is "?lhs = ?rhs")
+proof-
+  have os: "os_grant s (ChangeOwner p u)" and vs': "valid s" using vs
+    by (auto dest:valid_cons valid_os)
+  have "\<And> x. x \<noteq> p \<Longrightarrow> ?lhs x = ?rhs x"
+    by (auto simp:type_of_process.simps split:option.splits t_role.splits)
+  moreover have "?lhs p = ?rhs p"
+  proof-
+    from os have p_in: "p \<in> current_procs s" by (simp+)
+    then obtain r fr t u' where csp: "cp2sproc s p = Some (r, fr, t, u')" using vs'
+      by (drule_tac current_proc_has_sproc, auto)  
+    from os have "u \<in> init_users" by simp
+    hence "defrole u \<noteq> None" using init_user_has_role by (auto simp:bidirect_in_init_def)
+    then obtain nr where nrole:"chown_role_aux r fr u = Some nr"
+      by (case_tac fr, auto simp:chown_role_aux_def)
+    have nr_eq: "currentrole (ChangeOwner p u # s) p = chown_role_aux r fr u" 
+      using csp by (auto simp:chown_role_aux_valid'[where u = u])  
+    moreover have "type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)"
+      using csp nrole nr_eq 
+      by (rule_tac fr = fr and u' = u' in chown_type_aux_valid', simp+)
+    moreover have "proc_forcedrole (ChangeOwner p u # s) p = Some fr"
+      using csp by (auto split:option.splits)
+    moreover have "owner (ChangeOwner p u # s) p = Some u" by simp
+    ultimately have "cp2sproc (ChangeOwner p u # s) p = Some (nr, fr, chown_type_aux r nr t, u)" 
+      using nrole by (simp)
+    thus ?thesis using csp nrole by simp
+  qed
+  ultimately show ?thesis by (rule_tac ext, auto)
+qed
+
+lemma cp2sproc_crole:
+  "valid (ChangeRole p r # s) \<Longrightarrow> cp2sproc (ChangeRole p r # s) = (cp2sproc s) 
+     (p := (case (cp2sproc s p) of
+              Some (r',fr,pt,u) \<Rightarrow> Some (r,fr,pt,u)
+            | _                 \<Rightarrow> None)
+      )"
+apply (frule valid_cons, frule valid_os, simp)
+apply (frule current_proc_has_sproc, simp)
+apply (rule ext, auto split:option.splits)
+done
+
+lemma cp2sproc_exec:
+  assumes vs: "valid (Execute p f # s)"
+  shows "cp2sproc (Execute p f # s) = (cp2sproc s) 
+     (p := (case (cp2sproc s p, source_dir s f) of 
+              (Some (r,fr,pt,u), Some sd) \<Rightarrow> (
+     case (exec_role_aux r sd u, erole_functor init_file_forcedrole InheritUpMixed sd) of
+       (Some r', Some fr') \<Rightarrow> Some (r', fr', exec_type_aux r pt, u)
+     | _                   \<Rightarrow> None           )
+            | _                \<Rightarrow> None))" (is "?lhs = ?rhs")
+proof-
+  have os: "os_grant s (Execute p f)" and vs': "valid s" using vs
+    by (auto dest:valid_cons valid_os)
+  have "\<And> x. x \<noteq> p \<Longrightarrow> ?lhs x = ?rhs x"
+    by (auto simp:type_of_process.simps split:option.splits t_role.splits)
+  moreover have "?lhs p = ?rhs p"
+  proof-
+    from os have p_in: "p \<in> current_procs s" by (simp+)
+    then obtain r fr t u where csp: "cp2sproc s p = Some (r, fr, t, u)" using vs'
+      by (drule_tac current_proc_has_sproc, auto)  
+    from os have f_in: "f \<in> current_files s" by simp
+    then obtain sd where sdir: "source_dir s f = Some sd" using vs'
+      by (drule_tac current_file_has_sd, auto)
+    have "currentrole (Execute p f # s) p \<noteq> None" using vs p_in
+      by (rule_tac notI, drule_tac current_proc_has_role', simp+)
+    then obtain nr where nrole: "currentrole (Execute p f # s) p = Some nr" by auto
+    have "proc_forcedrole (Execute p f # s) p \<noteq> None" using vs p_in
+      by (rule_tac notI, drule_tac current_proc_has_forcedrole', simp+)
+    then obtain nfr where nfrole: "proc_forcedrole (Execute p f # s) p = Some nfr" by auto
+    have nr_eq: "currentrole (Execute p f # s) p = exec_role_aux r sd u" 
+      using csp f_in sdir vs' by (simp only:exec_role_aux_valid')
+    moreover have "type_of_process (Execute p f # s) p = Some (exec_type_aux r t)"
+      using csp by (simp only:exec_type_aux_valid')
+    moreover have nfr_eq: "proc_forcedrole (Execute p f # s) p = 
+                           erole_functor init_file_forcedrole InheritUpMixed sd" 
+      using sdir vs' f_in
+      apply (frule_tac source_dir_in_init, drule_tac source_dir_not_deleted)
+      by (simp add:undel_initf_keeps_efrole sd_deter_efrole)
+    moreover have "owner (Execute p f # s) p = Some u" using csp
+      by (auto split:option.splits)
+    ultimately have "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r t, u)" 
+      using nrole nfrole by (simp)
+    moreover have "exec_role_aux r sd u = Some nr" using nrole nr_eq by simp
+    moreover have "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"
+      using nfrole nfr_eq by simp
+    ultimately show ?thesis using csp sdir by simp 
+  qed
+  ultimately show ?thesis by (rule_tac ext, auto)
+qed
+
+lemma cp2sproc_clone:
+  "valid (Clone p p' # s) \<Longrightarrow> cp2sproc (Clone p p' # s) = (cp2sproc s) (p' := 
+      (case (cp2sproc s p) of
+         Some (r, fr, pt, u) \<Rightarrow> Some (r, fr, clone_type_aux r pt, u)
+       | _                   \<Rightarrow> None))"
+apply (frule valid_cons, frule valid_os)
+apply (rule ext, auto split:option.splits t_rc_proc_type.splits 
+                       simp:pct_def clone_type_aux_def
+                       dest:current_proc_has_type default_process_create_type_valid)
+done
+
+lemma cp2sproc_other:
+  "\<lbrakk>valid (e # s); \<forall> p f. e \<noteq> Execute p f; \<forall> p p'. e \<noteq> Clone p p';
+    \<forall> p r. e \<noteq> ChangeRole p r; \<forall> p u. e \<noteq> ChangeOwner p u\<rbrakk> \<Longrightarrow> cp2sproc (e#s) = cp2sproc s"
+by (case_tac e, auto)
+
+lemmas cp2sproc_simps = cp2sproc_exec cp2sproc_chown cp2sproc_crole cp2sproc_clone cp2sproc_other
+
+lemma obj2sobj_file: "obj2sobj s obj = SFile sf fopt \<Longrightarrow> \<exists> f. obj = File f"
+by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_proc: "obj2sobj s obj = SProc sp popt \<Longrightarrow> \<exists> p. obj = Proc p"
+by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_ipc: "obj2sobj s obj = SIPC si iopt \<Longrightarrow> \<exists> i. obj = IPC i"
+by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_file': 
+  "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> sf srf. sobj = SFile sf srf"
+by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_proc': 
+  "\<lbrakk>obj2sobj s (Proc p) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> sp srp. sobj = SProc sp srp"
+by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_ipc': 
+  "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> si sri. sobj =  SIPC si sri"
+by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)
+
+lemma obj2sobj_file_remains_cons:
+  assumes vs: "valid (e#s)" and exf: "f \<in> current_files s"
+  and SF: "obj2sobj s (File f) = SFile sf srf" 
+  and notdeled: "\<not> deleted (File f) (e#s)"
+  shows "obj2sobj (e#s) (File f) = SFile sf srf"
+proof-
+  from vs have os:"os_grant s e" and vs': "valid s" 
+    by (auto dest:valid_cons valid_os)
+  from notdeled exf have exf': "f \<in> current_files (e#s)" by (case_tac e, auto)
+  have "etype_of_file (e # s) f = etype_of_file s f"
+    using os vs vs' exf exf' 
+    apply (case_tac e, auto simp:etype_of_file_def split:option.splits) 
+    by (auto dest:ancient_file_in_current intro!:etype_aux_prop)
+  moreover have "source_dir (e # s) f = source_dir s f"
+    using os vs vs' exf exf'
+    by (case_tac e, auto simp:source_dir_simps dest:source_dir_prop)
+  ultimately show ?thesis using vs SF notdeled 
+    by (auto split:if_splits option.splits dest:not_deleted_cons_D)
+qed
+
+lemma obj2sobj_file_remains_cons':
+  "\<lbrakk>valid (e#s); f \<in> current_files s; obj2sobj s (File f) = SFile sf srf; no_del_event (e#s)\<rbrakk>
+   \<Longrightarrow> obj2sobj (e#s) (File f) = SFile sf srf"
+by (auto intro!:obj2sobj_file_remains_cons nodel_imp_un_deleted
+       simp del:obj2sobj.simps)
+
+lemma obj2sobj_file_remains':
+  "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (e#s); f \<in> current_files s;
+    no_del_event (e#s)\<rbrakk> \<Longrightarrow> obj2sobj (e#s) (File f) = sobj"
+apply (frule obj2sobj_file', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+apply (erule obj2sobj_file_remains_cons', simp+)
+done
+
+lemma obj2sobj_file_remains_app:
+  "\<lbrakk>obj2sobj s (File f) = SFile sf srf; valid (s' @ s); f \<in> current_files s;
+    \<not> deleted (File f) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = SFile sf srf"
+apply (induct s', simp)
+apply (simp only:cons_app_simp_aux)
+apply (frule valid_cons, frule not_deleted_cons_D)
+apply (drule_tac s = "s'@s" in obj2sobj_file_remains_cons, auto simp del:obj2sobj.simps)
+apply (drule_tac obj = "File f" in not_deleted_imp_exists', simp+)
+done
+
+lemma obj2sobj_file_remains_app':
+  "\<lbrakk>obj2sobj s (File f) = SFile sf srf; valid (s' @ s); f \<in> current_files s;
+    no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = SFile sf srf"
+by (auto intro!:obj2sobj_file_remains_app nodel_imp_un_deleted
+       simp del:obj2sobj.simps)
+
+lemma obj2sobj_file_remains'':
+  "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (s'@s); f \<in> current_files s;
+    no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = sobj"
+apply (frule obj2sobj_file', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+apply (erule obj2sobj_file_remains_app', simp+)
+done
+
+lemma obj2sobj_file_remains''':
+  "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (s'@s); f \<in> current_files s;
+    \<not>deleted (File f) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = sobj"
+apply (frule obj2sobj_file', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+by (erule obj2sobj_file_remains_app, simp+)
+
+lemma obj2sobj_ipc_remains_cons:
+  "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk>
+  \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"
+apply (frule valid_cons, frule valid_os, case_tac e)
+by (auto simp:ni_init_deled ni_notin_curi split:option.splits
+        dest!:current_proc_has_role')
+
+lemma obj2sobj_ipc_remains_cons':
+  "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk>
+  \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"
+by (auto intro!:obj2sobj_ipc_remains_cons nodel_imp_un_deleted
+       simp del:obj2sobj.simps)
+
+lemma obj2sobj_ipc_remains':
+  "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (e#s); i \<in> current_ipcs s; 
+    no_del_event (e#s)\<rbrakk> \<Longrightarrow> obj2sobj (e#s) (IPC i) = sobj"
+apply (frule obj2sobj_ipc', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+apply (erule obj2sobj_ipc_remains_cons', simp+)
+done
+
+lemma obj2sobj_ipc_remains_app:
+  "\<lbrakk>obj2sobj s (IPC i) = SIPC si sri; valid (s'@s); i \<in> current_ipcs s; \<not> deleted (IPC i) (s'@s)\<rbrakk>
+  \<Longrightarrow> obj2sobj (s'@s) (IPC i) = SIPC si sri"
+apply (induct s', simp)
+apply (simp only:cons_app_simp_aux)
+apply (frule valid_cons, frule not_deleted_cons_D)
+apply (drule_tac s = "s'@s" in obj2sobj_ipc_remains_cons, auto simp del:obj2sobj.simps)
+apply (drule_tac obj = "IPC i" in not_deleted_imp_exists', simp+)
+done
+
+lemma obj2sobj_ipc_remains_app':
+  "\<lbrakk>obj2sobj s (IPC i) = SIPC si sri; valid (s'@s); i \<in> current_ipcs s; no_del_event (s'@s)\<rbrakk>
+  \<Longrightarrow> obj2sobj (s'@s) (IPC i) = SIPC si sri"
+by (auto intro!:obj2sobj_ipc_remains_app nodel_imp_un_deleted
+       simp del:obj2sobj.simps)
+
+lemma obj2sobj_ipc_remains'':
+  "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (s'@s); i \<in> current_ipcs s; 
+    no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (IPC i) = sobj"
+apply (frule obj2sobj_ipc', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+apply (erule obj2sobj_ipc_remains_app', simp+)
+done
+
+lemma obj2sobj_ipc_remains''':
+  "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (s'@s); i \<in> current_ipcs s; 
+    \<not> deleted (IPC i) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (IPC i) = sobj"
+apply (frule obj2sobj_ipc', simp, (erule exE)+)
+apply (simp del:obj2sobj.simps)
+apply (erule obj2sobj_ipc_remains_app, simp+)
+done
+
+end
+
+context tainting_s_sound begin
+
+lemma cp2sproc_clone':
+  "valid (Clone p p' # s) \<Longrightarrow> cp2sproc (Clone p p' # s) = (cp2sproc s) (p' := cp2sproc s p)"
+by (drule cp2sproc_clone, auto split:option.splits simp:clone_type_unchange clone_type_aux_def)
+
+lemmas cp2sproc_simps' =  cp2sproc_exec cp2sproc_chown cp2sproc_crole cp2sproc_clone' cp2sproc_other
+
+lemma clone_sobj_keeps_same:
+  "valid (Clone p p' # s) \<Longrightarrow> obj2sobj (Clone p p' # s) (Proc p') = obj2sobj s (Proc p)"
+apply (frule valid_cons, frule valid_os, clarsimp)
+apply (auto split:option.splits t_rc_proc_type.splits
+             dest:current_proc_has_role current_proc_has_forcedrole 
+                  current_proc_has_type current_proc_has_owner default_process_create_type_valid
+             simp:pct_def clone_type_unchange)
+done
+
+end
+
+end
\ No newline at end of file