--- 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

--- a/Static.thy	Wed Sep 04 15:13:54 2013 +0800
+++ b/Static.thy	Thu Sep 05 13:23:03 2013 +0800
@@ -167,11 +167,12 @@
 
 fun is_many :: "t_sobject \<Rightarrow> bool"
 where
-  "is_many (S_proc (Many, sec, fds, shms) tag) = True"
-| "is_many (S_file sfs                    tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
-| "is_many (S_dir  sf                        ) = is_many_sfile sf"
-| "is_many (S_msgq sq                        ) = is_many_smsgq sq"
-| "is_many (S_shm  sh                        ) = is_many_sshm  sh"
+  "is_many (S_proc sp   tag) = is_many_sproc sp"
+| "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
+| "is_many (S_dir  sf      ) = is_many_sfile sf"
+| "is_many (S_msgq sq      ) = is_many_smsgq sq"
+| "is_many (S_shm  sh      ) = is_many_sshm  sh"
+| "is_many _                 = False"
 
 (*
 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"