--- a/S2ss_prop.thy	Wed Sep 04 15:13:54 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 05 13:23:03 2013 +0800
@@ -8,22 +8,6 @@
 
 (* simpset for s2ss*)
 
-lemma co2sobj_createshm:
-  "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
-      case obj of 
-        O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
-                                        Some sh \<Rightarrow> Some (S_shm sh)
-                                      | _       \<Rightarrow> None)
-                    else co2sobj s obj
-      | _        \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6 ch2sshm_simps
-             dest!:current_shm_has_sh'
-             dest:is_file_in_current is_dir_in_current)
-done
 
 lemma s2ss_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
@@ -36,6 +20,7 @@
                               \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
            | _ \<Rightarrow> s2ss s) )"
 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)
+
 apply (rule conjI, rule impI, (erule exE|erule conjE)+)
 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)
 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)
@@ -46,6 +31,14 @@
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (case_tac "obj = O_proc p")
 apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits)
+apply (simp add:co2sobj_execve, rule disjI2)
+apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]
+apply (simp, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
+apply (erule exE| erule conjE)+
+apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve)
 
 apply (case_tac obj, simp_all add:co2sobj_execve alive_simps)
 thm alive_execve