--- a/no_shm_selinux/Co2sobj_prop.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -1842,8 +1842,8 @@
 (* simpset for co2sobj *)
 
 lemma co2sobj_execve:
-  "\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
-      if (obj = O_proc p)
+  "\<lbrakk>valid (Execve p f fds # s); dalive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
+      if (obj = D_proc p)
       then (case (cp2sproc (Execve p f fds # s) p) of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
             | _       \<Rightarrow> None) 
@@ -1859,8 +1859,8 @@
 done
 
 lemma co2sobj_execve':
-  "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
-      if (obj = O_proc p)
+  "\<lbrakk>valid (Execve p f fds # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
+      if (obj = D_proc p)
       then (case (cp2sproc (Execve p f fds # s) p) of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
             | _       \<Rightarrow> None) 
@@ -1876,8 +1876,8 @@
 done
 
 lemma co2sobj_clone':
-  "\<lbrakk>valid (Clone p p' fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
-      if (obj = O_proc p')
+  "\<lbrakk>valid (Clone p p' fds # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
+      if (obj = D_proc p')
       then (case (cp2sproc (Clone p p' fds # s) p') of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
             | _       \<Rightarrow> None)
@@ -1895,9 +1895,9 @@
 done
 
 lemma co2sobj_clone:
-  "\<lbrakk>valid (Clone p p' fds # s); alive (Clone p p' fds # s) obj\<rbrakk> 
+  "\<lbrakk>valid (Clone p p' fds # s); dalive (Clone p p' fds # s) obj\<rbrakk> 
    \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
-      if (obj = O_proc p')
+      if (obj = D_proc p')
       then (case (cp2sproc (Clone p p' fds # s) p') of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
             | _       \<Rightarrow> None)
@@ -1920,7 +1920,7 @@
 
 (*
 lemma co2sobj_ptrace:
-  "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
+  "\<lbrakk>valid (Ptrace p p' # s); dalive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
      case obj of
        O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') 
                      then (case (cp2sproc s p'') of 
@@ -1945,9 +1945,9 @@
 *)
 
 lemma co2sobj_ptrace:
-  "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
+  "\<lbrakk>valid (Ptrace p p' # s); dalive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
      case obj of
-       O_proc p'' \<Rightarrow> if (p'' = p') 
+       D_proc p'' \<Rightarrow> if (p'' = p') 
                      then (case (cp2sproc s p'') of 
                              Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p \<in> tainted s))
                            | _       \<Rightarrow> None)
@@ -1955,7 +1955,7 @@
                           then (case (cp2sproc s p'') of 
                                   Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p' \<in> tainted s))
                                 | _       \<Rightarrow> None)
-                          else co2sobj s (O_proc p'')
+                          else co2sobj s (D_proc p'')
     | _          \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps cq2smsgq_other cf2sfiles_other)
@@ -1970,18 +1970,18 @@
 
 
 lemma co2sobj_open:
-  "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> 
+  "\<lbrakk>valid (Open p f flag fd opt # s); dalive (Open p f flag fd opt # s) obj\<rbrakk> 
    \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of 
-     O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
+     D_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
                   then (case (cf2sfile (Open p f flag fd opt # s) f) of
                           Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))
                         | _       \<Rightarrow> None)
-                  else co2sobj s (O_file f')
-   | O_proc p' \<Rightarrow> if (p' = p) 
+                  else co2sobj s (D_file f')
+   | D_proc p' \<Rightarrow> if (p' = p) 
                   then (case (cp2sproc (Open p f flag fd opt # s) p) of
                           Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
                         | _       \<Rightarrow> None)
-                  else co2sobj s (O_proc p')
+                  else co2sobj s (D_proc p')
    | _         \<Rightarrow> co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (auto simp:cp2sproc_simps split:option.splits
@@ -2015,7 +2015,7 @@
 
 (*
 lemma co2sobj_readfile:
-  "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
+  "\<lbrakk>valid (ReadFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
      case obj of
        O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
                        Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> tainted s)
@@ -2036,9 +2036,9 @@
 done
 *)
 lemma co2sobj_readfile:
-  "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
+  "\<lbrakk>valid (ReadFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
      case obj of
-       O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+       D_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
                        Some f \<Rightarrow> (if (p' = p \<and> O_file f \<in> tainted s)
                                   then (case (cp2sproc s p') of
                                           Some sp \<Rightarrow> Some (S_proc sp True)
@@ -2056,9 +2056,9 @@
 done
 
 lemma co2sobj_writefile:
-  "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
+  "\<lbrakk>valid (WriteFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
      case obj of
-       O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+       D_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
                        Some f \<Rightarrow> (if (f \<in> same_inode_files s f') 
                                   then Some (S_file (cf2sfiles s f') 
                                                     (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
@@ -2077,18 +2077,18 @@
 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 
 lemma co2sobj_closefd:
-  "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
+  "\<lbrakk>valid (CloseFd p fd # s); dalive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
       case obj of 
-        O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of 
+        D_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of 
                         Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
                                        f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. 
                                        f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-                                   then (case (cf2sfile s f, co2sobj s (O_file f')) of
+                                   then (case (cf2sfile s f, co2sobj s (D_file f')) of
                                            (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
                                          | _                              \<Rightarrow> None)
                                    else co2sobj s obj)
                      | _       \<Rightarrow> co2sobj s obj)
-      | O_proc p' \<Rightarrow> (if (p = p') 
+      | D_proc p' \<Rightarrow> (if (p = p') 
                       then (case (cp2sproc (CloseFd p fd # s) p) of
                               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
                             | _       \<Rightarrow> None)
@@ -2115,11 +2115,11 @@
 done
 
 lemma co2sobj_unlink:
-  "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
+  "\<lbrakk>valid (UnLink p f # s); dalive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
       case obj of
-        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
+        D_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
                         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-                     then (case (cf2sfile s f, co2sobj s (O_file f')) of
+                     then (case (cf2sfile s f, co2sobj s (D_file f')) of
                              (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
                            | _                              \<Rightarrow> None)
                      else co2sobj s obj
@@ -2142,7 +2142,7 @@
 done
 
 lemma co2sobj_rmdir:
-  "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
+  "\<lbrakk>valid (Rmdir p f # s); dalive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps cq2smsgq_other) (* ch2sshm_other*)
 apply (auto simp:cp2sproc_simps split:option.splits if_splits
@@ -2154,8 +2154,8 @@
 done
 
 lemma co2sobj_mkdir:
-  "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
-      if (obj = O_dir f) 
+  "\<lbrakk>valid (Mkdir p f i # s); dalive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
+      if (obj = D_dir f) 
       then (case (cf2sfile (Mkdir p f i # s) f) of 
               Some sf \<Rightarrow> Some (S_dir sf)
             | _       \<Rightarrow> None)
@@ -2171,10 +2171,10 @@
 done
 
 lemma co2sobj_linkhard:
-  "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 
+  "\<lbrakk>valid (LinkHard p oldf f # s); dalive (LinkHard p oldf f # s) obj\<rbrakk> 
    \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
     case obj of
-      O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
+      D_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
                    then (case (cf2sfile (LinkHard p oldf f # s) f) of
                            Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> tainted s))
                          | _       \<Rightarrow> None)
@@ -2197,9 +2197,9 @@
 done
 
 lemma co2sobj_truncate:
-  "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
+  "\<lbrakk>valid (Truncate p f len # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
       case obj of
-        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
+        D_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
                      then Some (S_file (cf2sfiles s f') (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
                      else co2sobj s obj
       | _         \<Rightarrow> co2sobj s obj)"
@@ -2213,7 +2213,7 @@
 done
 
 lemma co2sobj_kill:
-  "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
+  "\<lbrakk>valid (Kill p p' # s); dalive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) (* ch2sshm_other *)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
@@ -2223,7 +2223,7 @@
 done
 
 lemma co2sobj_exit:
-  "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
+  "\<lbrakk>valid (Exit p # s); dalive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
@@ -2233,9 +2233,9 @@
 done
 
 lemma co2sobj_createmsgq:
-  "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
+  "\<lbrakk>valid (CreateMsgq p q # s); dalive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
       case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
+        D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
                                          Some sq \<Rightarrow> Some (S_msgq sq)
                                        | _       \<Rightarrow> None)
                      else co2sobj s obj
@@ -2250,9 +2250,9 @@
 done
 
 lemma co2sobj_sendmsg:
-  "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
+  "\<lbrakk>valid (SendMsg p q m # s); dalive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
       case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
+        D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
                                          Some sq \<Rightarrow> Some (S_msgq sq)
                                        | _       \<Rightarrow> None)
                      else co2sobj s obj
@@ -2267,13 +2267,13 @@
 done
 
 lemma co2sobj_recvmsg:
-  "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
+  "\<lbrakk>valid (RecvMsg p q m # s); dalive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
       case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
+        D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
                                          Some sq \<Rightarrow> Some (S_msgq sq)
                                        | _       \<Rightarrow> None)
                      else co2sobj s obj
-      | O_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
+      | D_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
                      then (case (cp2sproc s p') of
                              Some sp \<Rightarrow> Some (S_proc sp True)
                            | _       \<Rightarrow> None)
@@ -2289,7 +2289,7 @@
 done
 (*
 lemma co2sobj_recvmsg:
-  "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
+  "\<lbrakk>valid (RecvMsg p q m # s); dalive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
       case obj of
         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
                                          Some sq \<Rightarrow> Some (S_msgq sq)
@@ -2312,7 +2312,7 @@
 *)
 
 lemma co2sobj_removemsgq:
-  "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> 
+  "\<lbrakk>valid (RemoveMsgq p q # s); dalive (RemoveMsgq p q # s) obj\<rbrakk> 
    \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
@@ -2325,7 +2325,7 @@
 
 (*
 lemma co2sobj_createshm:
-  "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
+  "\<lbrakk>valid (CreateShM p h # s); dalive (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)
@@ -2342,7 +2342,7 @@
 done
 
 lemma co2sobj_detach:
-  "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
+  "\<lbrakk>valid (Detach p h # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
       case obj of
         O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
                                          Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
@@ -2360,7 +2360,7 @@
 done
 
 lemma co2sobj_deleteshm:
-  "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
+  "\<lbrakk>valid (DeleteShM p h # s); dalive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
       case obj of
         O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
                         Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> tainted s))
@@ -2385,7 +2385,7 @@
 by (simp add:info_flow_shm_def)
 
 lemma co2sobj_attach:
-  "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
+  "\<lbrakk>valid (Attach p h flag # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
       case obj of
         O_proc p' \<Rightarrow> if (info_flow_shm s p p')
                      then (case (cp2sproc (Attach p h flag # s) p') of
@@ -2426,8 +2426,45 @@
 done
 *)
 
+lemma co2sobj_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> co2sobj (Bind p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+
+lemma co2sobj_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> co2sobj (Connect p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+
+lemma co2sobj_createsock:
+  "valid (CreateSock p af st fd inum # s) \<Longrightarrow> co2sobj (CreateSock p af st fd inum # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+
+lemma co2sobj_accept:
+  "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> co2sobj (Accept p fd addr port fd' inum # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+
+lemma co2sobj_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> co2sobj (Listen p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_sendsock:
+  "valid (SendSock p fd # s) \<Longrightarrow> co2sobj (SendSock p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_recvsock:
+  "valid (RecvSock p fd # s) \<Longrightarrow> co2sobj (RecvSock p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_shutdown:
+  "valid (Shutdown p fd addr # s) \<Longrightarrow> co2sobj (Shutdown p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+
 lemma co2sobj_other:
-  "\<lbrakk>valid (e # s); alive (e # s) obj; 
+  "\<lbrakk>valid (e # s); dalive (e # s) obj; 
     \<forall> p f fds. e \<noteq> Execve p f fds;
     \<forall> p p' fds. e \<noteq> Clone p p' fds;
     \<forall> p p'. e \<noteq> Ptrace p p';
@@ -2456,8 +2493,8 @@
   co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
   co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
   co2sobj_removemsgq (* co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm *)
-
-
+  co2sobj_createsock co2sobj_accept co2sobj_listen co2sobj_sendsock co2sobj_recvsock 
+  co2sobj_shutdown co2sobj_bind co2sobj_connect
 
 end
 

--- a/no_shm_selinux/Enrich2.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -956,6 +956,17 @@
     by auto
 qed
 
+fun enrich_file_link :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_state)"
+where
+  "enrich_file_link [] tf df = []"
+
+fun enrich_file_set :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> t_state"
+where
+  "enrich_file_set [] tf df = []"
+| "enrich_file_set [] (Open p f flags fd (Some inum) # s) = 
+    
+
+
 
 
 lemma enrich_msgq_s2ss:

--- a/no_shm_selinux/Init_prop.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Init_prop.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -791,7 +791,7 @@
 *)
 
 lemma co2sobj_nil_prop:
-  "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
+  "init_dalive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
 apply (case_tac obj)
 apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop 
                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
@@ -802,9 +802,15 @@
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 done
 
+lemma init_dalive_prop: "init_dalive obj = dalive [] obj"
+apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props
+         is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil
+         is_tcp_sock_nil is_udp_sock_nil)
+done
+
 lemma s2ss_nil_prop:
   "s2ss [] = init_static_state"
-using co2sobj_nil_prop init_alive_prop
+using co2sobj_nil_prop init_dalive_prop
 by (auto simp add:s2ss_def init_static_state_def)
 
 end

--- a/no_shm_selinux/S2ss_prop.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/S2ss_prop.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory S2ss_prop
-imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop
+imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop Dalive_prop
 begin
 (*>*)
 
@@ -8,22 +8,9 @@
 
 (* simpset for s2ss*)
 
-lemma co2sobj_some_case:
-  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);
-    \<And> f. obj = O_file f \<Longrightarrow> P (O_file f);
-    \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>
-   \<Longrightarrow> P obj" (*  \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h); *)
-by (case_tac obj, auto)
-
-lemma co2sobj_execve_alive:
-  "\<lbrakk>alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\<rbrakk>
-   \<Longrightarrow> alive (Execve p f fds # s) obj"
-apply (erule co2sobj_some_case)
-by (auto simp:alive_simps simp del:alive.simps)
-
 lemma s2ss_execve':
   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
-     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (D_proc p') = co2sobj s (D_proc p))
      then (case (cp2sproc (Execve p f fds # s) p) of
              Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}
            | _ \<Rightarrow> {} )
@@ -41,19 +28,18 @@
 apply (erule exE, simp)
 apply (simp add:s2ss_def, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj_execve 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 (rule_tac x = obj in exI, case_tac obj, (simp add:dalive_simps)+)[1]
 apply (simp, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp)
+apply (rule_tac x = "D_proc p" in exI, simp)
 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 cp2sproc_execve)
-apply (case_tac "obj = O_proc p", simp)
-apply (frule co2sobj_execve_alive, simp, simp)
-apply (frule_tac obj = obj in co2sobj_execve, simp)
+apply (rule_tac x = "D_proc p'" in exI)
+apply (simp add:dalive_execve co2sobj_execve cp2sproc_execve)
+apply (case_tac "obj = D_proc p", simp, simp add:dalive_execve)
+apply (frule_tac obj = obj in co2sobj_execve, simp add:dalive_execve)
 apply (rule_tac x = obj in exI, simp, simp)
 
 apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)
@@ -62,26 +48,20 @@
 apply (erule exE, erule conjE, simp)
 apply (simp add:s2ss_def, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
-apply (case_tac "obj = O_proc p", simp)
+apply (case_tac "obj = D_proc p", simp)
 apply (rule disjI1, simp split:if_splits)
 apply (simp add:co2sobj_execve, rule disjI2)
-apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+apply (rule conjI,rule_tac x = obj in exI, simp add:dalive_simps split:t_object.splits)
 apply (rule notI, simp, case_tac obj)
 apply (erule_tac x = nat in allE, simp, (simp split:option.splits)+)
 apply (erule disjE, simp)
-apply (rule_tac x = "O_proc p" in exI, simp)
+apply (rule_tac x = "D_proc p" in exI, simp)
 apply (erule exE|erule conjE)+
-apply (rule_tac x = obj in exI)
-apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)
-apply (frule_tac obj = obj in co2sobj_execve, simp, simp)
+apply (rule_tac x = obj in exI, simp add:dalive_execve)
+apply (frule_tac obj = obj in co2sobj_execve, simp add:dalive_execve, simp)
 apply (rule impI, simp, simp)
 done
 
-lemma s2ss_clone_alive:
-  "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds # s)\<rbrakk>
-   \<Longrightarrow> alive (Clone p p' fds # s) obj"
-by (erule co2sobj_some_case, auto simp:alive_clone)
-
 lemma s2ss_clone:
   "valid (Clone p p' fds # s) \<Longrightarrow> s2ss (Clone p p' fds # s) = (
      case (cp2sproc (Clone p p' fds # s) p') of
@@ -91,21 +71,23 @@
 apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
 apply (rule allI, rule impI, simp add:s2ss_def)
 apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)
-apply (case_tac "obj = O_proc p'", simp)
+apply (case_tac "obj = D_proc p'", simp)
 apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)
 apply (rule disjI1, simp split:if_splits)
 apply (simp, rule disjI2)
 apply (frule co2sobj_clone, simp)
-apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+apply (rule_tac x = obj in exI)
+apply (simp add:dalive_simps split:t_dobject.splits)
 
 apply (simp, erule disjE, simp)
-apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (rule_tac x = "D_proc p'" in exI, simp)
 apply (rule impI, rule notI, drule tainted_in_current, simp+)
 apply (erule exE| erule conjE)+
-apply (case_tac "obj = O_proc p'", simp)
+apply (case_tac "obj = D_proc p'", simp)
 apply (rule_tac x = obj in exI)
-apply (frule s2ss_clone_alive, simp+)
-apply (auto simp:co2sobj_clone alive_simps)
+apply (frule dalive_clone)
+apply (case_tac obj)
+apply (auto simp:co2sobj_clone split:t_dobject.splits simp del:co2sobj.simps)
 done
 
 (*
@@ -167,6 +149,7 @@
                 else tainted s)"
 by auto
 
+(*
 lemma co2sobj_some_caseD:
   "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);
     \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 
@@ -174,11 +157,12 @@
     \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>
    \<Longrightarrow> P obj"
 by (case_tac obj, auto)
+*)
 
-definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
 where
   "update_s2ss_obj s ss obj sobj sobj' = 
-     (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+     (if (\<exists> obj'. dalive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
       then ss \<union> {sobj'}
       else ss - {sobj} \<union> {sobj'})"
 
@@ -218,26 +202,26 @@
 *}
 
 lemma co2sobj_sproc_imp:
-  "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"
+  "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = D_proc p"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
 lemma co2sobj_sfile_imp:
-  "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"
+  "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = D_file f"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
 lemma co2sobj_sdir_imp:
-  "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"
+  "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = D_dir f"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
 lemma co2sobj_smsgq_imp:
-  "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
+  "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = D_msgq q"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
 lemma s2ss_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> 
      (case (cp2sproc s p, cp2sproc (Execve p f fds # s) p) of
         (Some sp, Some sp') \<Rightarrow> s2ss (Execve p f fds # s) = 
-            update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))
+            update_s2ss_obj s (s2ss s) (D_proc p) (S_proc sp (O_proc p \<in> tainted s))
                           (S_proc sp' (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
       | _ \<Rightarrow> s2ss (Execve p f fds # s) = {})"
 apply (frule vd_cons, frule vt_grant_os)
@@ -257,7 +241,7 @@
 apply (rule impI)
 apply (tactic {*my_clarify_tac 1*})
 apply (simp split:option.splits)
-apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (erule_tac x = "D_proc p'" in allE, simp)
 done
 
 lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp
@@ -266,7 +250,7 @@
   "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> tainted s; O_proc p' \<notin> tainted s\<rbrakk>
    \<Longrightarrow> (case (cp2sproc s p') of 
           Some sp' \<Rightarrow> s2ss (Ptrace p p' # s) = 
-                     update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp' False) (S_proc sp' True)
+                     update_s2ss_obj s (s2ss s) (D_proc p') (S_proc sp' False) (S_proc sp' True)
         | _        \<Rightarrow> s2ss (Ptrace p p' # s) = {})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (clarsimp simp only:os_grant.simps)
@@ -279,36 +263,36 @@
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p'")
+apply (case_tac "obj = D_proc p'")
 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps dalive_other split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p'")
+apply (case_tac "obj = D_proc p'")
 apply (rule_tac x = obj' in exI)
-apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace dalive_other split:t_dobject.splits if_splits)
 apply (auto simp:co2sobj.simps)[1]
-apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace dalive_other split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p'")
+apply (case_tac "obj = D_proc p'")
 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps dalive_other split:t_dobject.splits if_splits)
 apply (rule notI, simp)
 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)
 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p'")
+apply (case_tac "obj = D_proc p'")
 apply (simp add:co2sobj.simps cp2sproc_other)
-apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace dalive_other split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 done
 
@@ -316,7 +300,7 @@
   "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> tainted s; O_proc p \<notin> tainted s\<rbrakk>
    \<Longrightarrow> (case (cp2sproc s p) of 
           Some sp \<Rightarrow> s2ss (Ptrace p p' # s) = 
-                    update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+                    update_s2ss_obj s (s2ss s) (D_proc p) (S_proc sp False) (S_proc sp True)
         | _       \<Rightarrow> s2ss (Ptrace p p' # s) = {})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (clarsimp simp only:os_grant.simps)
@@ -329,36 +313,36 @@
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps dalive_other split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI)
-apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace dalive_other split:t_dobject.splits if_splits)
 apply (auto simp:co2sobj.simps)[1]
-apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace dalive_other split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)
+apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps dalive_other split:t_dobject.splits if_splits)
 apply (rule notI, simp)
 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)
 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps cp2sproc_other)
-apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace dalive_other split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 done
 
@@ -369,31 +353,31 @@
 apply (frule vd_cons, frule vt_grant_os, rule set_eqI, rule iffI)
 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = obj in exI)
-apply (frule alive_other, simp+)
+apply (frule dalive_other, simp+)
 apply (frule_tac obj = obj in co2sobj_ptrace, simp)
-apply (auto split:t_object.splits option.splits if_splits)[1]
+apply (auto split:t_dobject.splits option.splits if_splits)[1]
 
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (frule alive_other, simp+)
+apply (frule dalive_other, simp+)
 apply (frule_tac obj = obj in co2sobj_ptrace, simp)
 apply (case_tac "cp2sproc s p'")
 apply (drule current_proc_has_sp', simp, simp)
 apply (case_tac "cp2sproc s p")
 apply (drule current_proc_has_sp', simp, simp)
 apply (case_tac "O_proc p' \<in> tainted s")
-apply (auto split:t_object.splits option.splits if_splits simp:co2sobj.simps)
+apply (auto split:t_dobject.splits option.splits if_splits simp:co2sobj.simps)
 done
 
 lemma s2ss_ptrace:
   "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (
      if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 
      then (case (cp2sproc s p') of 
-             Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp False) (S_proc sp True)
+             Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (D_proc p') (S_proc sp False) (S_proc sp True)
            | _       \<Rightarrow> {})
      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)
           then (case (cp2sproc s p) of 
-                  Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+                  Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (D_proc p) (S_proc sp False) (S_proc sp True)
                 | _       \<Rightarrow> {})
           else s2ss s                                   )"
 apply (case_tac "O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s")
@@ -405,9 +389,9 @@
 
 lemma s2ss_kill':
   "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (
-     if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))
+     if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (D_proc p'') = co2sobj s (D_proc p'))
      then s2ss s 
-     else (case (co2sobj s (O_proc p')) of
+     else (case (co2sobj s (D_proc p')) of
              Some sp \<Rightarrow> s2ss s - {sp}
            | _       \<Rightarrow> {}))"
 apply (frule vt_grant_os, frule vd_cons)
@@ -419,42 +403,42 @@
 apply (simp split: option.splits, (erule conjE)+)
 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
+apply (simp add:co2sobj_kill dalive_kill split:t_dobject.splits if_splits)
 apply (erule CollectE, erule exE, erule conjE, rule CollectI)
-apply (erule co2sobj_some_caseD)
-apply (case_tac "pa = p'")
-apply (rule_tac x = "O_proc p''" in exI)
-apply (simp add:cp2sproc_kill alive_kill
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_kill alive_kill
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+apply (case_tac obj)
+apply (case_tac "nat = p'")
+apply (rule_tac x = "D_proc p''" in exI)
+apply (simp add:cp2sproc_kill dalive_kill
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = "D_proc nat" in exI)
+apply (clarsimp simp add:cp2sproc_kill dalive_kill
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule dalive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
 
 apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)
 apply (rule set_eqI, rule iffI)
 apply (erule CollectE, erule exE, erule conjE, rule DiffI)
 apply (rule CollectI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)
+apply (simp add:co2sobj_kill dalive_kill split:t_dobject.splits if_splits)
 apply (rule notI, simp, case_tac obj)
 apply (erule_tac x = nat in allE)
 apply (simp add:co2sobj_kill cp2sproc_kill split:option.splits)
 apply (simp split:option.splits)+
-apply (erule co2sobj_some_caseD)
-apply (case_tac "pa = p'")
-apply (rule_tac x = "O_proc p''" in exI)
-apply (simp add:cp2sproc_kill alive_kill
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_kill alive_kill
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+apply (case_tac obj)
+apply (case_tac "nat = p'")
+apply (rule_tac x = "D_proc p''" in exI)
+apply (simp add:cp2sproc_kill dalive_kill
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = "D_proc nat" in exI)
+apply (clarsimp simp add:cp2sproc_kill dalive_kill
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule dalive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
 done
 
-definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
 where
   "del_s2ss_obj s ss obj sobj \<equiv> 
-     if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+     if (\<exists> obj'. dalive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
      then ss
      else ss - {sobj}"
 
@@ -465,7 +449,7 @@
 lemma s2ss_kill:
   "valid (Kill p p' # s) \<Longrightarrow> (
       case (cp2sproc s p') of 
-        Some sp \<Rightarrow> s2ss (Kill p p' # s) = del_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp (O_proc p' \<in> tainted s))
+        Some sp \<Rightarrow> s2ss (Kill p p' # s) = del_s2ss_obj s (s2ss s) (D_proc p') (S_proc sp (O_proc p' \<in> tainted s))
       | _       \<Rightarrow> s2ss (Kill p p' # s) = {})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (clarsimp simp only:os_grant.simps)
@@ -483,14 +467,14 @@
 apply (rule impI)
 apply (tactic {*my_clarify_tac 1*})
 apply (simp split:option.splits)
-apply (erule_tac x = "O_proc p''" in allE, simp)
+apply (erule_tac x = "D_proc p''" in allE, simp)
 done
 
 lemma s2ss_exit':
   "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (
-     if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (D_proc p') = co2sobj s (D_proc p))
      then s2ss s 
-     else (case (co2sobj s (O_proc p)) of
+     else (case (co2sobj s (D_proc p)) of
              Some sp \<Rightarrow> s2ss s - {sp}
            | _       \<Rightarrow> {}))"
 apply (frule vt_grant_os, frule vd_cons)
@@ -502,42 +486,42 @@
 apply (simp split: option.splits, (erule conjE)+)
 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
+apply (simp add:co2sobj_exit dalive_exit split:t_dobject.splits if_splits)
 apply (erule CollectE, erule exE, erule conjE, rule CollectI)
-apply (erule co2sobj_some_caseD)
-apply (case_tac "pa = p")
-apply (rule_tac x = "O_proc p'" in exI)
-apply (simp add:cp2sproc_exit alive_exit
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_exit alive_exit
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+apply (case_tac obj)
+apply (case_tac "nat = p")
+apply (rule_tac x = "D_proc p'" in exI)
+apply (simp add:cp2sproc_exit dalive_exit
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = "D_proc nat" in exI)
+apply (clarsimp simp add:cp2sproc_exit dalive_exit
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule dalive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
 
 apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)
 apply (rule set_eqI, rule iffI)
 apply (erule CollectE, erule exE, erule conjE, rule DiffI)
 apply (rule CollectI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)
+apply (simp add:co2sobj_exit dalive_exit split:t_dobject.splits if_splits)
 apply (rule notI, simp, case_tac obj)
 apply (erule_tac x = nat in allE)
 apply (simp add:co2sobj_exit cp2sproc_exit split:option.splits)
 apply (simp split:option.splits)+
-apply (erule co2sobj_some_caseD)
-apply (case_tac "pa = p")
-apply (rule_tac x = "O_proc p'" in exI)
-apply (simp add:cp2sproc_exit alive_exit
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = "O_proc pa" in exI)
-apply (clarsimp simp add:cp2sproc_exit alive_exit
-  split:t_object.splits if_splits option.splits)
-apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+apply (case_tac obj)
+apply (case_tac "nat = p")
+apply (rule_tac x = "D_proc p'" in exI)
+apply (simp add:cp2sproc_exit dalive_exit
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = "D_proc nat" in exI)
+apply (clarsimp simp add:cp2sproc_exit dalive_exit
+  split:t_dobject.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule dalive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
 done
 
 lemma s2ss_exit:
   "valid (Exit p # s) \<Longrightarrow> (
       case (cp2sproc s p) of 
-        Some sp \<Rightarrow> s2ss (Exit p # s) = del_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))
+        Some sp \<Rightarrow> s2ss (Exit p # s) = del_s2ss_obj s (s2ss s) (D_proc p) (S_proc sp (O_proc p \<in> tainted s))
       | _       \<Rightarrow> s2ss (Exit p # s) = {})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (clarsimp simp only:os_grant.simps)
@@ -555,11 +539,11 @@
 apply (rule impI)
 apply (tactic {*my_clarify_tac 1*})
 apply (simp split:option.splits)
-apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (erule_tac x = "D_proc p'" in allE, simp)
 done
 
-lemma alive_has_sobj':
-  "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
+lemma dalive_has_sobj':
+  "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> dalive s obj"
 apply (case_tac obj)
 apply (auto split:option.splits)
 oops
@@ -567,163 +551,141 @@
 declare co2sobj.simps [simp del]
 
 lemma co2sobj_open_none:
-  "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
-      if (obj = O_proc p) 
+  "\<lbrakk>valid (Open p f flag fd None # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
+      if (obj = D_proc p) 
       then (case (cp2sproc (Open p f flag fd None # s) p) of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
            | _       \<Rightarrow> None)
       else co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons)
-apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
-apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+apply (frule_tac obj = obj in co2sobj_open, simp add:dalive_open)
+apply (auto split:t_dobject.splits option.splits dest!:current_proc_has_sp')
 done
 
 lemma co2sobj_open_some:
-  "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (
-      if (obj = O_proc p) 
+  "\<lbrakk>valid (Open p f flag fd (Some i) # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (
+      if (obj = D_proc p) 
       then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of
               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
            | _       \<Rightarrow> None)
-      else if (obj = O_file f) 
+      else if (obj = D_file f) 
            then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of
                    Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))
                  | _       \<Rightarrow> None)
            else co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons)
-apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
-apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+apply (frule_tac obj = obj in co2sobj_open, simp add:dalive_open)
+apply (auto split:t_dobject.splits option.splits dest!:current_proc_has_sp')
 done
 
-lemma alive_co2sobj_some_open_none:
-  "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>
-   \<Longrightarrow> alive (Open p f flag fd None # s) obj"
-by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
-
-lemma alive_co2sobj_some_open_none':
-  "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 
-    valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"
-by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
-
 lemma co2sobj_proc_obj:
-  "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>
-   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+  "\<lbrakk>co2sobj s obj = Some x; co2sobj s (D_proc p) = Some x\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = D_proc p'"
 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
 
 lemma s2ss_open_none:
   "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (
-      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of
+      case (co2sobj s (D_proc p), co2sobj (Open p f flag fd None # s) (D_proc p)) of
         (Some sp, Some sp') \<Rightarrow> 
-           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (D_proc p') = Some sp)
            then s2ss s \<union> {sp'}
            else s2ss s - {sp} \<union> {sp'} 
       | _                   \<Rightarrow> {} )"
 unfolding s2ss_def
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (case_tac "co2sobj s (D_proc p)", simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
-apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")
+apply (case_tac "co2sobj (Open p f flag fd None # s) (D_proc p)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)
-apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)
+apply (simp add:dalive_open)
 apply (rule conjI, rule impI, erule exE, (erule conjE)+)
-apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = D_proc p", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none dalive_open split:t_dobject.splits)
 apply (rule impI)
-apply (case_tac "obj = O_proc p", simp)
+apply (case_tac "obj = D_proc p", simp)
 apply (rule Meson.disj_comm, rule disjCI, rule conjI)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none split:t_dobject.splits)
+apply (rule notI)
 apply (simp add:co2sobj_open_none split:option.splits)
-apply (rule notI)
-apply (frule co2sobj_proc_obj, simp, erule exE)
-apply (erule_tac x = p' in allE, simp)
+apply (frule_tac co2sobj_proc_obj, simp, erule exE)
+apply (erule_tac x = p' in allE, simp split:t_dobject.splits)
 
 apply (simp split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
-apply (erule exE, erule conjE, case_tac "obj = O_proc p")
-apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
-apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")
-apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp)
+apply (erule exE, erule conjE, case_tac "obj = D_proc p")
+apply (rule_tac x = "D_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none dalive_open)
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp)
+apply (erule conjE, erule exE, erule conjE, case_tac "obj = D_proc p")
+apply (rule_tac x = "D_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none dalive_open)
 done
 
-lemma alive_co2sobj_some_open_some:
-  "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>
-   \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"
-by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)
-
-lemma alive_co2sobj_some_open_some':
-  "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 
-    valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"
-by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
-
 lemma s2ss_open_some:
   "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (
-      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),
-            co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of
+      case (co2sobj s (D_proc p), co2sobj (Open p f flag fd (Some i) # s) (D_proc p),
+            co2sobj (Open p f flag fd (Some i) # s) (D_file f)) of
         (Some sp, Some sp', Some sf) \<Rightarrow> 
-           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (D_proc p') = Some sp)
            then s2ss s \<union> {sp', sf} 
            else s2ss s - {sp} \<union> {sp', sf} 
       | _                   \<Rightarrow> {} )"
 unfolding s2ss_def
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (case_tac "co2sobj s (D_proc p)", simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
-apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (D_proc p)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
-apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (D_file f)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (clarsimp split del:if_splits)
 
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
 apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)
-apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (case_tac "obj = D_proc p", simp, case_tac "obj = D_file f", simp)
 apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
-apply (simp add:co2sobj_open split:t_object.splits)
-apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (simp add:co2sobj_open dalive_open split:t_dobject.splits option.splits)
+apply (rule impI, case_tac "obj = D_proc p", simp, case_tac "obj = D_file f", simp)
 apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
-apply (simp add:co2sobj_open split:t_object.splits)
+apply (simp add:co2sobj_open dalive_open split:t_dobject.splits)
 apply (frule_tac obj = obj in co2sobj_open_some, simp+)
-apply (simp add:alive_co2sobj_some_open_some', simp)
-apply (rule notI)
+apply (simp add:dalive_open)
+apply (rule notI, simp)
 apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)
 apply (erule_tac x = p' in allE, simp)
 
 apply (simp split:if_splits, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp)
-apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (rule_tac x = "D_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "D_file f" in exI, simp add:is_file_simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p", simp)
-apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)
-apply (case_tac "obj = O_file f", simp add:is_file_in_current)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
-apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (case_tac "obj = D_proc p", simp)
+apply (rule_tac x = "D_proc p'" in exI, simp add:co2sobj_open_some)
+apply (case_tac "obj = D_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some dalive_open)
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "D_file f" in exI, simp add:is_file_simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p", simp)
-apply (case_tac "obj = O_file f", simp add:is_file_in_current)
-apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
+apply (case_tac "obj = D_proc p", simp)
+apply (case_tac "obj = D_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some dalive_open)
 done
 
 lemma s2ss_open':
   "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (
      if opt = None
-     then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of
+     then (case (co2sobj s (D_proc p), co2sobj (Open p f flag fd opt # s) (D_proc p)) of
         (Some sp, Some sp') \<Rightarrow> 
-           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (D_proc p') = Some sp)
            then s2ss s \<union> {sp'}
            else s2ss s - {sp} \<union> {sp'} 
       | _                   \<Rightarrow> {} )
-     else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),
-            co2sobj (Open p f flag fd opt # s) (O_file f)) of
+     else (case (co2sobj s (D_proc p), co2sobj (Open p f flag fd opt # s) (D_proc p),
+            co2sobj (Open p f flag fd opt # s) (D_file f)) of
         (Some sp, Some sp', Some sf) \<Rightarrow> 
-           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (D_proc p') = Some sp)
            then s2ss s \<union> {sp', sf} 
            else s2ss s - {sp} \<union> {sp', sf} 
       | _                   \<Rightarrow> {} ) )"
@@ -732,40 +694,40 @@
 done
 
 lemma co2sobj_proc_eq_some:
-  "\<lbrakk>co2sobj s (O_proc p) = Some sp; co2sobj s obj = Some sp\<rbrakk>
-   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+  "\<lbrakk>co2sobj s (D_proc p) = Some sp; co2sobj s obj = Some sp\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = D_proc p'"
 apply (case_tac obj, case_tac[!] sp)
 by (auto simp:co2sobj.simps split:option.splits)
 
 lemma s2ss_open:
   "valid (Open p f flag fd opt # s) \<Longrightarrow> 
-    (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p), 
-           co2sobj (Open p f flag fd opt # s) (O_file f)) of
+    (case (co2sobj s (D_proc p), co2sobj (Open p f flag fd opt # s) (D_proc p), 
+           co2sobj (Open p f flag fd opt # s) (D_file f)) of
        (Some sp, Some sp', Some sf) \<Rightarrow> s2ss (Open p f flag fd opt # s) = (
        if opt = None
-       then update_s2ss_obj s (s2ss s) (O_proc p) sp sp'
-       else update_s2ss_obj s (s2ss s) (O_proc p) sp sp' \<union> {sf})
+       then update_s2ss_obj s (s2ss s) (D_proc p) sp sp'
+       else update_s2ss_obj s (s2ss s) (D_proc p) sp sp' \<union> {sf})
      | _ \<Rightarrow> s2ss (Open p f flag fd opt # s) = {})"
 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)
-apply (case_tac "co2sobj s (O_proc p)")
+apply (case_tac "co2sobj s (D_proc p)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (drule current_proc_has_sp', simp, simp)
-apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_proc p)")
+apply (case_tac "co2sobj (Open p f flag fd opt # s) (D_proc p)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (drule current_proc_has_sp', simp, simp)
 apply (drule current_proc_has_sp', simp, simp)
-apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_file f)")
+apply (case_tac "co2sobj (Open p f flag fd opt # s) (D_file f)")
 apply (simp add:co2sobj.simps split:option.splits)
 apply (simp split:option.splits add:s2ss_open' update_s2ss_obj_def)
 apply (auto)
-apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (erule_tac x = "D_proc p'" in allE, simp)
 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
 apply (erule_tac x = "p'" in allE, simp)
-apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (erule_tac x = "D_proc p'" in allE, simp)
 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
 apply (erule_tac x = "p'" in allE, simp)
-apply (erule_tac x = "O_proc p'" in allE, simp)
+apply (erule_tac x = "D_proc p'" in allE, simp)
 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)
 apply (erule_tac x = "p'" in allE, simp)
 done
@@ -775,7 +737,7 @@
      case (file_of_proc_fd s p fd) of 
        Some f \<Rightarrow> if (O_file f \<in> tainted s \<and> O_proc p \<notin> tainted s)
                  then (case (cp2sproc s p) of 
-                         Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)
+                         Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (D_proc p) (S_proc sp False) (S_proc sp True)
                        | _       \<Rightarrow> {})
                  else s2ss s
      | _      \<Rightarrow> {})"
@@ -789,44 +751,44 @@
 apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI1, simp add:co2sobj_readfile)
 apply (rule disjI2, simp)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)
+apply (simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x= "O_proc p" in exI, simp add:alive_other co2sobj_readfile)
+apply (rule_tac x= "D_proc p" in exI, simp add:dalive_other co2sobj_readfile)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p")
-apply (rule_tac x = "O_proc pa" in exI, simp add:alive_other co2sobj_readfile)
+apply (case_tac "obj = D_proc p")
+apply (rule_tac x = "D_proc pa" in exI, simp add:dalive_other co2sobj_readfile)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (auto simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits)[1]
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI1, simp add:co2sobj_readfile)
 apply (rule disjI2, rule DiffI)
 apply (simp, rule_tac x = obj in exI)
-apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)
+apply (simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits)
 apply (rule notI, erule_tac x = obj in allE)
-apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (auto simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits)[1]
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:alive_other co2sobj_readfile)
+apply (rule_tac x = "D_proc p" in exI, simp add:dalive_other co2sobj_readfile)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]
+apply (auto simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits)[1]
 apply (simp add:co2sobj.simps)
 
 apply (simp add:s2ss_def, rule impI)
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)
+apply (simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits if_splits)
 apply (simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)
+apply (auto simp add:dalive_other co2sobj_readfile split:t_dobject.splits option.splits if_splits)
 apply (simp add:co2sobj.simps)
 done
 
@@ -845,10 +807,10 @@
 done
 
 lemma co2sobj_writefile_unchange:
-  "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;
+  "\<lbrakk>valid (WriteFile p fd # s); dalive s obj; file_of_proc_fd s p fd = Some f;
     O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk> 
    \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"
-apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)
+apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_dobject.splits if_splits)
 apply (simp add:co2sobj.simps)
 apply (case_tac "O_proc p \<in> tainted s")
 apply (simp add:same_inodes_tainted)+
@@ -859,7 +821,7 @@
      case (file_of_proc_fd s p fd) of
        Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)
                  then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>
-                                 co2sobj s (O_file f') = co2sobj s (O_file f))
+                                 co2sobj s (D_file f') = co2sobj s (D_file f))
                        then s2ss s \<union> {S_file (cf2sfiles s f) True}
                        else s2ss s - {S_file (cf2sfiles s f) False} 
                                    \<union> {S_file (cf2sfiles s f) True})
@@ -870,49 +832,44 @@
 unfolding s2ss_def
 apply (rule conjI|rule impI|erule exE|erule conjE)+
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
-apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)
-apply (simp split:t_object.splits if_splits)
-apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)
+apply (frule_tac obj =  obj in co2sobj_writefile, simp add:dalive_other)
+apply (simp split:t_dobject.splits if_splits)
+apply (rule disjI2, rule_tac x= "D_proc nat" in exI, simp)
 apply (rule disjI1, simp add:cf2sfiles_prop)
 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)
-apply (simp add:co2sobj.simps)
 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (rule disjI2, rule_tac x = obj in exI, simp)
 apply (rule disjI2, rule_tac x = obj in exI, simp)
 apply (simp add:co2sobj.simps)
 
 apply (erule disjE)
-apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)
-apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)
+apply (rule_tac x = "D_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)
+apply (frule_tac obj = "D_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)
 apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)
 apply (erule exE, erule conjE, erule conjE)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
-apply (case_tac "fa \<in> same_inode_files s aa")
-apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)
-apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (case_tac "list \<in> same_inode_files s aa")
+apply (frule_tac f = list and f' = aa in cf2sfiles_prop, simp)
+apply (rule_tac x = "D_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
 apply (rule conjI, rule impI, simp add:same_inode_files_prop5)
 apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)
-apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule_tac x = "D_file list" in exI, simp add:co2sobj_writefile is_file_simps)
 apply (rule impI, simp add:same_inode_files_prop5)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
 
 apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)
-apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)
-apply (simp add:co2sobj_writefile split:t_object.splits if_splits)
+apply (rule CollectI, rule_tac x = obj in exI, simp add:dalive_simps)
+apply (simp add:co2sobj_writefile split:t_dobject.splits if_splits)
 apply (simp add:co2sobj.simps same_inodes_tainted)
 apply (case_tac "O_proc p \<in> tainted s", simp, simp)
 apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_writefile_unchange alive_simps)
+apply (simp add:co2sobj_writefile_unchange dalive_simps)
 
 apply (rule impI| rule conjI|erule conjE)+
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
-apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)
+apply (simp add:dalive_simps co2sobj_writefile split:t_dobject.splits)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
   rule notI, simp add:co2sobj.simps split:option.splits)
 apply (simp split:if_splits)
@@ -921,43 +878,39 @@
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (erule_tac x = list in allE, simp add:same_inode_files_prop5)
 apply (simp add:co2sobj.simps)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
-  rule notI, simp add:co2sobj.simps split:option.splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
-  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp split:option.splits add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
   rule notI, simp add:co2sobj.simps split:option.splits)
 apply (simp add:co2sobj.simps)
 apply (erule disjE)
-apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)
+apply (rule_tac x= "D_file aa" in exI)
+apply ( simp add:co2sobj_writefile dalive_simps file_of_pfd_is_file)
 apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)
 apply (erule exE|erule conjE)+
-apply (erule co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
-apply (case_tac "fa \<in> same_inode_files s aa")
+apply (case_tac "list \<in> same_inode_files s aa")
 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)
 apply (rule impI, simp add:same_inode_files_prop5)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+
 apply (rule impI, rule impI)
-
 apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_writefile_unchange alive_simps)
+apply (simp add:co2sobj_writefile_unchange dalive_simps)
 apply (erule CollectE, erule exE, erule conjE)
 apply (rule CollectI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_writefile_unchange alive_simps)
+apply (simp add:co2sobj_writefile_unchange dalive_simps)
 done
 
 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
 where
  "update_s2ss_sfile_tainted s ss f tag \<equiv>
     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> 
-              co2sobj s (O_file f') = Some (S_file (cf2sfiles s f) False))
+              co2sobj s (D_file f') = Some (S_file (cf2sfiles s f) False))
        then ss \<union> {S_file (cf2sfiles s f) True}
        else ss - {S_file (cf2sfiles s f) False} 
                \<union> {S_file (cf2sfiles s f) True}"
@@ -989,38 +942,36 @@
   "del_s2ss_file s ss f sf = 
      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
       then ss
-      else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
+      else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (D_file f') = co2sobj s (D_file f))
            then update_s2ss_sfile_del s ss f sf
            else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)}) f sf)"
 
 
-lemma alive_co2sobj_closefd1:
-  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
+lemma dalive_co2sobj_closefd1:
+  "\<lbrakk>dalive s obj; valid (CloseFd p fd # s); 
     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
-   \<Longrightarrow> alive (CloseFd p fd # s) obj"
-apply (erule co2sobj_some_caseD)
-by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
-
-lemma alive_co2sobj_closefd3:
-  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;
-    file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
-   \<Longrightarrow> alive (CloseFd p fd # s) obj"
-apply (erule co2sobj_some_caseD)
-by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+   \<Longrightarrow> dalive (CloseFd p fd # s) obj"
+apply (case_tac obj)
+by (auto simp:dalive_simps is_file_simps is_dir_simps split:option.splits)
 
-lemma alive_co2sobj_closefd2:
-  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>
-   \<Longrightarrow> alive (CloseFd p fd # s) obj"
-apply (erule co2sobj_some_caseD)
-by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+lemma dalive_co2sobj_closefd3:
+  "\<lbrakk>dalive s obj; valid (CloseFd p fd # s); obj \<noteq> D_file f;
+    file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
+   \<Longrightarrow> dalive (CloseFd p fd # s) obj"
+apply (case_tac obj)
+by (auto simp:dalive_simps is_file_simps is_dir_simps split:option.splits)
 
-lemma alive_co2sobj_closefd':
-  "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 
-    valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"
-apply (erule co2sobj_some_caseD)
-by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)
+lemma dalive_co2sobj_closefd2:
+  "\<lbrakk>dalive s obj; valid (CloseFd p fd # s); file_of_proc_fd s p fd = None\<rbrakk>
+   \<Longrightarrow> dalive (CloseFd p fd # s) obj"
+apply (case_tac obj)
+by (auto simp:dalive_simps is_file_simps is_dir_simps split:option.splits)
 
-ML {*asm_full_simp_tac*}
+lemma dalive_co2sobj_closefd':
+  "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; dalive (CloseFd p fd # s) obj; 
+    valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> dalive s obj"
+apply (case_tac obj)
+by (auto simp:dalive_simps is_file_simps is_dir_simps split:option.splits if_splits)
 
 lemma same_inode_files_prop10:
   "\<lbrakk>same_inode_files s f \<noteq> {f}; is_file s f\<rbrakk> \<Longrightarrow> \<exists> f'. f' \<in> same_inode_files s f \<and> f' \<noteq> f"
@@ -1041,13 +992,13 @@
                  then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
                          (Some sf, Some sp, Some sp') \<Rightarrow> 
                             (del_s2ss_file s (
-                               update_s2ss_obj s (s2ss s) (O_proc p) 
+                               update_s2ss_obj s (s2ss s) (D_proc p) 
                                  (S_proc sp (O_proc p \<in> tainted s))
                                  (S_proc sp' (O_proc p \<in> tainted s))) f sf)
                       | _ \<Rightarrow> {})
                  else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 
                          (Some sp, Some sp') \<Rightarrow> 
-                            (update_s2ss_obj s (s2ss s) (O_proc p)
+                            (update_s2ss_obj s (s2ss s) (D_proc p)
                                (S_proc sp (O_proc p \<in> tainted s))
                                (S_proc sp' (O_proc p \<in> tainted s)))
                       | _ \<Rightarrow> {})
@@ -1059,17 +1010,17 @@
 
 apply (simp add:s2ss_def)
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
-apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (rule_tac x = obj in exI, simp add:dalive_co2sobj_closefd')
 apply (frule co2sobj_closefd, simp)
 apply (frule cp2sproc_closefd, simp)
-apply (simp add:proc_file_fds_def split:t_object.splits)
+apply (simp add:proc_file_fds_def split:t_dobject.splits)
 apply (simp split:if_splits add:co2sobj.simps)
 apply (erule CollectE, erule exE, erule conjE, rule CollectI)
-apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
+apply (rule_tac x = obj in exI, simp add:dalive_co2sobj_closefd2)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_co2sobj_closefd2)
 apply (frule cp2sproc_closefd, simp)
 apply (auto simp add:proc_file_fds_def co2sobj.simps 
-            split:t_object.splits option.splits if_splits)[1]
+            split:t_dobject.splits option.splits if_splits)[1]
 
 apply (case_tac "cp2sproc (CloseFd p fd # s) p")
 apply (drule current_proc_has_sp', simp, simp)
@@ -1085,177 +1036,177 @@
 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
 apply (tactic {*my_seteq_tac 1*})
 apply simp
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_simps)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI)
+apply (rule_tac x = "D_proc p" in exI)
 apply (simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI)
 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "obj = D_file a")
+apply (rule_tac x = "D_file f'" in exI)
 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)[1]
 
 apply (rule impI)+
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps)
+apply (case_tac "obj = D_proc p", rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2)
-apply (case_tac "obj = O_file a", simp add:alive_simps)
+apply (case_tac "obj = D_file a", simp add:dalive_simps)
 apply (rule DiffI, simp)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd', simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (erule_tac x = "O_proc pa" in allE, simp)
+apply (erule_tac x = "D_proc pa" in allE, simp)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)
+apply (case_tac "obj = D_proc p", simp add:co2sobj.simps)
+apply (case_tac "obj = D_file a", rule_tac x = "D_file f'" in exI)
 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 
 apply (rule impI, tactic {*my_seteq_tac 1*})
 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
-apply (case_tac "f = a", simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
+apply (case_tac "list = a", simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule disjI1)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (erule bexE, erule conjE)
 apply (erule_tac x = f'' in ballE, simp, simp)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule impI, rule conjI, rule impI)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
-apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "list = a", simp add:dalive_simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 apply (rule impI)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (rule notI, simp add:co2sobj_closefd)
 apply (erule_tac x = obj in allE, simp)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule disjI1)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (erule bexE, erule conjE)
 apply (erule_tac x = f'' in ballE, simp, simp)
 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
 apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI)
 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "obj = D_file a")
+apply (rule_tac x = "D_file f'" in exI)
 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (auto simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "obj = D_file a")
+apply (rule_tac x = "D_file f'" in exI)
 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (erule disjE)
 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'a" in exI)
+apply (rule_tac x = "D_file f'a" in exI)
 apply (frule same_inode_files_prop11)
-apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
-apply (simp add:alive_simps)+
+apply (frule_tac obj = "D_file f'a" in co2sobj_closefd)
+apply (simp add:dalive_simps)+
 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI)
 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_closefd)
-apply (case_tac "f \<in> same_inode_files s a")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "list \<in> same_inode_files s a")
+apply (rule_tac x = "D_file f'" in exI)
 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
@@ -1267,25 +1218,25 @@
 
 apply (erule disjE)
 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'a" in exI)
+apply (rule_tac x = "D_file f'a" in exI)
 apply (frule same_inode_files_prop11)
-apply (frule_tac obj = "O_file f'a" in co2sobj_closefd)
-apply (simp add:alive_simps)+
+apply (frule_tac obj = "D_file f'a" in co2sobj_closefd)
+apply (simp add:dalive_simps)+
 apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule disjE)
-apply (rule_tac x = "O_proc p" in exI)
+apply (rule_tac x = "D_proc p" in exI)
 apply (simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_closefd)
-apply (case_tac "f \<in> same_inode_files s a")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "list \<in> same_inode_files s a")
+apply (rule_tac x = "D_file f'" in exI)
 apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits)
 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
@@ -1299,107 +1250,107 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
-apply (case_tac "f = a", simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
+apply (case_tac "list = a", simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:dalive_simps split:if_splits)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
-apply (rule notI, simp, erule_tac x = "O_proc pa" in allE, simp add:co2sobj_closefd)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
+apply (rule notI, simp, erule_tac x = "D_proc nat" in allE, simp add:co2sobj_closefd)
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule disjI2)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (erule bexE, erule conjE)
-apply (rule conjI, rule_tac x = "O_file f''" in exI)
+apply (rule conjI, rule_tac x = "D_file f''" in exI)
 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule notI, simp)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
 apply (erule bexE, erule conjE)
 apply (simp add:update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI)
 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (case_tac "obj = D_file a")
+apply (rule_tac x = "D_file f'" in exI)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps same_inode_files_prop11)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule conjI)
 apply (rule impI)
 apply (rule_tac x = f' in ballE, simp, simp, simp)
 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (auto simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)[1]
+apply (erule disjE, rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)
+apply (case_tac "obj = D_file a")
+apply (rule_tac x = "D_file f'" in exI)
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd, simp add:dalive_simps same_inode_files_prop11)
+apply (simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)
 apply (rule conjI)
 apply (rule impI)
 apply (rule_tac x = f' in ballE, simp, simp, simp)
 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:dalive_simps co2sobj.simps split:t_dobject.splits if_splits)[1]
 
 apply (rule impI)
 apply (tactic {*my_seteq_tac 1*})
 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
-apply (case_tac "f = a", simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
+apply (case_tac "list = a", simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:alive_simps split:if_splits)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, clarsimp simp:dalive_simps split:if_splits)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp)
 apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits)
 apply (erule_tac x= f in allE, simp add:co2sobj.simps)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule notI, simp)
 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule disjI1)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (erule bexE, erule conjE)
@@ -1407,25 +1358,25 @@
 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
 apply (simp add:is_file_simps co2sobj_closefd)
 apply (rule notI, simp add:co2sobj_closefd)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps) 
+apply (erule_tac x = list in allE, simp add:is_file_simps co2sobj.simps) 
 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule impI, rule conjI, rule impI)
 
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule notI, simp)
 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule conjI, rule disjI2, rule conjI)
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule conjI, rule disjI2, rule conjI)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps)
 apply (rule notI, simp add:co2sobj.simps)
@@ -1433,24 +1384,24 @@
 apply (simp add:is_file_simps co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps)
 apply (rule notI, simp add:co2sobj_closefd)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
+apply (erule_tac x = list in allE, simp add:is_file_simps co2sobj.simps)
 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 apply (rule impI)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (case_tac "pa = p", simp add:co2sobj.simps)
+apply (case_tac obj)
+apply (case_tac "nat = p", simp add:co2sobj.simps)
 apply (rule disjI2, rule notI, simp)
 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a", rule disjI1)
 apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp)
@@ -1458,86 +1409,86 @@
 apply (simp add:is_file_simps co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps)
 apply (rule notI, simp add:co2sobj_closefd)
-apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps)
+apply (erule_tac x = list in allE, simp add:is_file_simps co2sobj.simps)
 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
 apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
 apply (erule conjE, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_file a", simp add:co2sobj.simps)
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
-apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj' in dalive_co2sobj_closefd3, simp+)
 apply (simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (erule conjE|erule exE|erule disjE)+
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_file a", simp add:co2sobj.simps)
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
-apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]
+apply (auto simp add:co2sobj.simps split:t_dobject.splits if_splits)[1]
 apply (erule conjE|erule exE|erule disjE)+
 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'" in exI)
+apply (rule_tac x = "D_file f'" in exI)
 apply (frule same_inode_files_prop11)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
-apply (simp add:alive_simps)+
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd)
+apply (simp add:dalive_simps)+
 apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule conjE, erule disjE)
-apply (rule_tac x = "O_proc p" in exI)
+apply (rule_tac x = "D_proc p" in exI)
 apply (simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
-apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj' in dalive_co2sobj_closefd3, simp+)
 apply (simp add:co2sobj_closefd)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_file a", simp add:co2sobj.simps)
+apply (frule_tac obj = obj in dalive_co2sobj_closefd3, simp+)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_closefd)
-apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a")
+apply (case_tac "list = a", simp add:dalive_simps)
+apply (case_tac "list \<in> same_inode_files s a")
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 apply (erule disjE)
 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'" in exI)
+apply (rule_tac x = "D_file f'" in exI)
 apply (frule same_inode_files_prop11)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
-apply (simp add:alive_simps)+
+apply (frule_tac obj = "D_file f'" in co2sobj_closefd)
+apply (simp add:dalive_simps)+
 apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits)
 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule conjE, erule disjE)
-apply (rule_tac x = "O_proc p" in exI)
+apply (rule_tac x = "D_proc p" in exI)
 apply (simp add:co2sobj.simps)
 apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)
-apply (case_tac "obj = O_file a", simp add:co2sobj.simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_proc p", simp add:co2sobj.simps)
+apply (case_tac "obj = D_file a", simp add:co2sobj.simps)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_closefd)
-apply (case_tac "f \<in> same_inode_files s a")
+apply (case_tac "list \<in> same_inode_files s a")
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
@@ -1549,47 +1500,47 @@
 apply (simp add:s2ss_def)
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
 apply (simp)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps split:if_splits)
 apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
-apply (simp add:alive_co2sobj_closefd')
-apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
+apply (simp add:dalive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_dobject.splits if_splits)
 apply (simp, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
-apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
-apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp:co2sobj.simps)
-apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp: co2sobj.simps)
+apply (case_tac "obj = D_proc p")
+apply (rule_tac x = obj' in exI, simp add:dalive_co2sobj_closefd1)
+apply (frule_tac obj = obj' in co2sobj_closefd, simp add:dalive_co2sobj_closefd1)
+apply (clarsimp split:t_dobject.splits if_splits option.splits simp:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:dalive_co2sobj_closefd1)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_co2sobj_closefd1)
+apply (clarsimp split:t_dobject.splits if_splits option.splits simp: co2sobj.simps)
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
 apply (simp)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI1, simp add:co2sobj.simps split:if_splits)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits simp: co2sobj.simps)
-apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:dalive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_co2sobj_closefd1)
+apply (clarsimp split:t_dobject.splits if_splits option.splits simp: co2sobj.simps)
+apply (rule notI, erule_tac x = obj in allE, simp add:dalive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_co2sobj_closefd1)
+apply (clarsimp split:t_dobject.splits if_splits option.splits)
 apply (simp)
 apply (erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps)
 apply (erule exE|erule conjE)+
 apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
-apply (clarsimp split:t_object.splits if_splits option.splits 
-                simp: co2sobj.simps alive_co2sobj_closefd1)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:dalive_co2sobj_closefd1)
+apply (clarsimp split:t_dobject.splits if_splits option.splits 
+                simp: co2sobj.simps dalive_co2sobj_closefd1)
 done
 
-lemma alive_co2sobj_unlink:
-  "\<lbrakk>alive s obj; valid (UnLink p f # s); obj \<noteq> O_file f\<rbrakk>
-   \<Longrightarrow> alive (UnLink p f # s) obj"
-by (auto simp add:alive_simps split:t_object.splits)
+lemma dalive_co2sobj_unlink:
+  "\<lbrakk>dalive s obj; valid (UnLink p f # s); obj \<noteq> D_file f\<rbrakk>
+   \<Longrightarrow> dalive (UnLink p f # s) obj"
+by (auto simp add:dalive_simps split:t_dobject.splits)
 
 lemma s2ss_unlink:
   "valid (UnLink p f # s) \<Longrightarrow> s2ss (UnLink p f # s) = (
@@ -1607,33 +1558,31 @@
 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:is_file_simps)
+apply (case_tac "obj = D_file f", simp add:is_file_simps)
 apply simp
 apply (rule conjI)
-apply (rule_tac x = obj in exI,simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI,simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)
 apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp)
 apply (frule_tac obj = obj in co2sobj_unlink, simp)
 apply (erule_tac x = fa in allE, simp add:is_file_simps)
 apply (simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
-apply (frule_tac alive_co2sobj_unlink, simp, simp)
+apply (case_tac "obj = D_file f", simp add:co2sobj.simps)
+apply (frule_tac dalive_co2sobj_unlink, simp, simp)
 apply (frule_tac obj = obj in co2sobj_unlink, simp)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj.simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps split:t_dobject.splits if_splits)
 
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
 
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:alive_simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_file f", simp add:dalive_simps)
+apply (case_tac obj)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_unlink)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1)
 apply (simp add:co2sobj_unlink)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
@@ -1644,8 +1593,8 @@
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
 apply (tactic {*my_setiff_tac 1*})
 apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps)
-apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (rule_tac x = "D_file f'a" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "D_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop 
   is_file_simps same_inode_files_prop11 split:if_splits)
 apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
@@ -1653,14 +1602,14 @@
 
 apply (tactic {*my_setiff_tac 1*})
 apply (case_tac "f' = f", simp add:same_inode_files_prop9) 
-apply (case_tac "obj= O_file f")
-apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
+apply (case_tac "obj= D_file f")
+apply (rule_tac x = "D_file f'" in exI, simp add:is_file_simps)
 apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
 apply (simp add:co2sobj.simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "list \<in> same_inode_files s f")
+apply (rule_tac x = "D_file f'" in exI)
 apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
 apply (simp add:co2sobj.simps is_file_simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
@@ -1672,12 +1621,12 @@
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:alive_simps, simp)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_file f", simp add:dalive_simps, simp)
+apply (case_tac obj)
 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_unlink)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1)
 apply (simp add:co2sobj_unlink)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits)
@@ -1685,24 +1634,24 @@
 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_unlink is_file_simps)
 apply (rule notI, simp add:co2sobj_unlink)
-apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps)
+apply (erule_tac x = list in allE, simp add:co2sobj.simps is_file_simps)
 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
-apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
-apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (rule_tac x = "D_file f'" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "D_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop 
   is_file_simps same_inode_files_prop11 split:if_splits)
 apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
 apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
 apply (tactic {*my_setiff_tac 1*}, simp)
-apply (case_tac "obj = O_file f", simp add:co2sobj.simps)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_file f", simp add:co2sobj.simps)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
@@ -1712,45 +1661,39 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (subgoal_tac "alive (UnLink p f # s) obj")
-apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
-apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
+apply (subgoal_tac "dalive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)[1]
+apply (auto simp add:co2sobj_unlink dalive_simps split:t_dobject.splits)[1]
 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:alive_simps)
-apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (case_tac "obj = D_file f", simp add:dalive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (case_tac "obj = D_file f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)[1]
 apply (rule_tac x =obj in exI)
-apply (subgoal_tac "alive (UnLink p f # s) obj")
-apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
-apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
+apply (subgoal_tac "dalive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits)[1]
+apply (auto simp add:co2sobj_unlink dalive_simps split:t_dobject.splits)[1]
 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:alive_simps)
-apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (case_tac "obj = D_file f", simp add:dalive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps same_inode_files_prop9 split:t_object.splits)[1]
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "obj = D_file f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps same_inode_files_prop9 split:t_dobject.splits)[1]
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (simp add:alive_simps co2sobj.simps)
+apply (case_tac "list \<in> same_inode_files s f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (simp add:dalive_simps co2sobj.simps)
 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
 apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink)
 apply (simp add:current_files_simps is_file_simps is_file_in_current)
@@ -1761,27 +1704,25 @@
 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f", simp add:alive_simps)
-apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (case_tac "obj = D_file f", simp add:dalive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (case_tac "obj = D_file f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (subgoal_tac "dalive (UnLink p f # s) (D_file f')")
 apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
-apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (frule_tac obj = "D_file f'" in co2sobj_unlink, simp)
 apply (simp split:if_splits option.splits add:is_file_simps)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (auto split:t_sobject.splits)[1]
 apply (simp add:is_file_simps same_inode_files_prop11)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (case_tac "list \<in> same_inode_files s f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (subgoal_tac "dalive (UnLink p f # s) (D_file f')")
 apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
-apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (frule_tac obj = "D_file f'" in co2sobj_unlink, simp)
 apply (simp split:if_splits option.splits add:is_file_simps)
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
 apply (auto split:t_sobject.splits)[1]
@@ -1792,8 +1733,8 @@
 done
 
 lemma s2ss_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> s2ss (Rmdir p f # s) = (
-  case (co2sobj s (O_dir f)) of
-    Some sdir \<Rightarrow> del_s2ss_obj s (s2ss s) (O_dir f) sdir
+  case (co2sobj s (D_dir f)) of
+    Some sdir \<Rightarrow> del_s2ss_obj s (s2ss s) (D_dir f) sdir
   | _         \<Rightarrow> {})"
 apply (frule vd_cons, frule vt_grant_os)
 apply (clarsimp simp:dir_is_empty_def)
@@ -1806,30 +1747,30 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_rmdir is_file_simps is_dir_simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj_rmdir is_file_simps is_dir_simps dalive_simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_dir f")
+apply (case_tac "obj = D_dir f")
 apply (rule_tac x = obj' in exI)
-apply (subgoal_tac "alive (Rmdir p f # s) obj'")
-apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
-apply (simp add:alive_rmdir)
+apply (subgoal_tac "dalive (Rmdir p f # s) obj'")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_dobject.splits)[1]
+apply (simp add:dalive_rmdir)
 apply (rule_tac x = obj in exI)
-apply (subgoal_tac "alive (Rmdir p f # s) obj")
-apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
-apply (simp add:alive_rmdir)
+apply (subgoal_tac "dalive (Rmdir p f # s) obj")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_dobject.splits)[1]
+apply (simp add:dalive_rmdir)
 
 apply (rule conjI|rule impI|erule exE|erule conjE)+
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply simp
-apply (case_tac "obj = O_dir f", simp add:alive_rmdir)
+apply (case_tac "obj = D_dir f", simp add:dalive_rmdir)
 apply (rule conjI)
-apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir dalive_rmdir)
 apply (simp add:co2sobj_rmdir)
-apply (simp add:alive_rmdir, erule_tac x = obj in allE, simp)
+apply (simp add:dalive_rmdir, erule_tac x = obj in allE, simp)
 apply (tactic {*my_setiff_tac 1*}, simp)
-apply (case_tac "obj = O_dir f", simp)
-apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+apply (case_tac "obj = D_dir f", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir dalive_rmdir)
 done
 
 lemma s2ss_mkdir: "valid (Mkdir p f inum # s) \<Longrightarrow> s2ss (Mkdir p f inum # s) = (
@@ -1842,20 +1783,20 @@
 
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*}, simp)
-apply (case_tac "obj = O_dir f")
+apply (case_tac "obj = D_dir f")
 apply (rule disjI1, simp add:co2sobj.simps)
-apply (rule disjI2, rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:co2sobj_mkdir dalive_simps)
 apply (tactic {*my_setiff_tac 1*}, simp)
-apply (rule_tac x = "O_dir f" in exI, simp add:alive_mkdir co2sobj.simps)
+apply (rule_tac x = "D_dir f" in exI, simp add:dalive_mkdir co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)
-apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
+apply (case_tac "obj = D_dir f", simp add:is_dir_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir dalive_mkdir)
 done
 
 definition update_s2ss_sfile_add :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 where
  "update_s2ss_sfile_add s ss f sf \<equiv>
-    if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
+    if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (D_file f') = co2sobj s (D_file f))
        then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}
        else ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)} 
                \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> tainted s)}"
@@ -1873,54 +1814,54 @@
 apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f'")
+apply (case_tac "obj = D_file f'")
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard
   same_inode_files_linkhard split:if_splits)
 apply (case_tac "O_file f' \<in> tainted s")
-apply (drule tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (drule tainted_in_current, simp, simp add:is_file_in_current dalive.simps, simp)
+apply (case_tac obj)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj_linkhard dalive_linkhard)
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard 
   same_inodes_tainted split:if_splits)
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
-apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
-apply (simp add:alive_linkhard)
-apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (rule_tac x = "D_file f" in exI)
+apply (frule_tac obj = "D_file f" in co2sobj_linkhard)
+apply (simp add:dalive_linkhard)
+apply (simp add:dalive_linkhard same_inode_files_prop9 split:t_dobject.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "obj = D_file f'", simp add:dalive_linkhard is_file_in_current)
+apply (case_tac obj)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (case_tac "list \<in> same_inode_files s f")
+apply (rule_tac x = "D_file f'a" in exI, simp add:co2sobj_linkhard dalive_linkhard)
 apply (rule conjI, rule impI, simp add:is_file_in_current)
 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
 
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f'", simp)
+apply (case_tac "obj = D_file f'", simp)
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard
   same_inode_files_linkhard split:if_splits)
 apply (case_tac "O_file f' \<in> tainted s")
-apply (drule tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
-apply (erule_tac obj = obj in co2sobj_some_caseD, simp)
+apply (drule tainted_in_current, simp, simp add:is_file_in_current dalive.simps, simp)
+apply (case_tac obj, simp)
 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_linkhard alive_linkhard)
+apply (simp add:co2sobj_linkhard dalive_linkhard)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard 
   same_inodes_tainted split:if_splits)
 apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
-apply (erule_tac x = fa in allE, rule notI)
+apply (erule_tac x = list in allE, rule notI)
 apply (simp add:co2sobj_linkhard is_file_simps)
 apply (simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
@@ -1928,19 +1869,19 @@
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
-apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
-apply (simp add:alive_linkhard)
-apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (rule_tac x = "D_file f" in exI)
+apply (frule_tac obj = "D_file f" in co2sobj_linkhard)
+apply (simp add:dalive_linkhard)
+apply (simp add:dalive_linkhard same_inode_files_prop9 split:t_dobject.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "obj = D_file f'", simp add:dalive_linkhard is_file_in_current)
+apply (case_tac obj)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (case_tac "list \<in> same_inode_files s f")
 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
-apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard dalive_linkhard)
 done
 
 lemma same_inode_files_prop12:
@@ -1958,11 +1899,11 @@
 apply (rule conjI|rule impI|erule exE|erule conjE)+
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f")
+apply (case_tac "obj = D_file f")
 apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac obj)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate dalive_simps)
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
@@ -1971,14 +1912,14 @@
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
+apply (rule_tac x = "D_file f" in exI)
 apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
-apply (case_tac "fa \<in> same_inode_files s f")
-apply (rule_tac x = "O_file f'" in exI)
-apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (case_tac "list \<in> same_inode_files s f")
+apply (rule_tac x = "D_file f'" in exI)
+apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_dobject.splits)[1]
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -1987,17 +1928,17 @@
 apply (rule conjI|rule impI|erule exE|erule conjE)+
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_file f")
+apply (case_tac "obj = D_file f")
 apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other)
-apply (erule_tac obj = obj in co2sobj_some_caseD)
-apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
+apply (case_tac obj)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate dalive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
 apply (rule notI, simp add:co2sobj_truncate is_file_simps)
-apply (erule_tac x = fa in allE)
+apply (erule_tac x = list in allE)
 apply (simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_dir_simps)
@@ -2006,12 +1947,12 @@
 apply (simp add:co2sobj_truncate)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_file f" in exI)
+apply (rule_tac x = "D_file f" in exI)
 apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
-apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac obj)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
-apply (case_tac "fa \<in> same_inode_files s f")
+apply (case_tac "list \<in> same_inode_files s f")
 apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
@@ -2020,14 +1961,14 @@
 apply (rule impI, simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_simps co2sobj_truncate)
-apply (simp split:t_object.splits if_splits add:co2sobj.simps)
+apply (simp add:dalive_simps co2sobj_truncate)
+apply (simp split:t_dobject.splits if_splits add:co2sobj.simps)
 apply (case_tac "O_proc p \<in> tainted s", simp add:same_inodes_tainted)
 apply simp
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_simps co2sobj_truncate)
-apply (auto split:t_object.splits if_splits simp:co2sobj.simps same_inodes_tainted)
+apply (simp add:dalive_simps co2sobj_truncate)
+apply (auto split:t_dobject.splits if_splits simp:co2sobj.simps same_inodes_tainted)
 done
 
 lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \<Longrightarrow> s2ss (CreateMsgq p q # s) = 
@@ -2039,24 +1980,22 @@
 apply (drule current_has_smsgq', simp+)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_createmsgq is_file_simps is_dir_simps split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj_createmsgq is_file_simps is_dir_simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply simp
 apply (rule_tac x = obj in exI)
-apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits)
+apply (auto simp add:co2sobj_createmsgq dalive_simps split:t_dobject.splits if_splits)
 done
 
 lemma s2ss_sendmsg: "valid (SendMsg p q m # s) \<Longrightarrow> s2ss (SendMsg p q m # s) = (
   case (cq2smsgq s q, cq2smsgq (SendMsg p q m # s) q) of
-    (Some sq, Some sq') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+    (Some sq, Some sq') \<Rightarrow> update_s2ss_obj s (s2ss s) (D_msgq q) (S_msgq sq) (S_msgq sq')
   | _  \<Rightarrow> {})"
 apply (frule vd_cons, frule vt_grant_os, clarsimp)
 apply (case_tac "cq2smsgq s q")
@@ -2068,55 +2007,49 @@
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
-apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_dobject.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
-apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule_tac x = obj' in exI)
-apply (simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits if_splits)
+apply (simp add:co2sobj_sendmsg dalive_sendmsg split:t_dobject.splits if_splits)
 apply (auto simp:co2sobj.simps)[1]
-apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg dalive_sendmsg split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_dobject.splits if_splits)
 apply (rule notI, simp)
 apply (frule_tac obj = obj in co2sobj_smsgq_imp, erule exE, simp)
 apply (erule_tac x = obj in allE, simp add:co2sobj_sendmsg)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (simp add:co2sobj.simps)
-apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg dalive_sendmsg split:t_dobject.splits)
 apply (auto simp:co2sobj.simps)[1]
 done
 
-lemma alive_co2sobj_removemsgq:
-  "\<lbrakk>alive s obj; valid (RemoveMsgq p q # s); co2sobj s obj = Some sobj; obj \<noteq> O_msgq q\<rbrakk> 
-   \<Longrightarrow> alive (RemoveMsgq p q # s) obj"
-apply (erule co2sobj_some_caseD)
+lemma dalive_co2sobj_removemsgq:
+  "\<lbrakk>dalive s obj; valid (RemoveMsgq p q # s); obj \<noteq> D_msgq q\<rbrakk> 
+   \<Longrightarrow> dalive (RemoveMsgq p q # s) obj"
+apply (case_tac obj)
 apply (auto simp:is_file_simps is_dir_simps)
 done
 
 lemma s2ss_removemsgq: "valid (RemoveMsgq p q # s) \<Longrightarrow> s2ss (RemoveMsgq p q # s) = 
   (case (cq2smsgq s q) of
-     Some sq \<Rightarrow> del_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq)
+     Some sq \<Rightarrow> del_s2ss_obj s (s2ss s) (D_msgq q) (S_msgq sq)
    | _       \<Rightarrow> {})"
 apply (frule vd_cons, frule vt_grant_os, clarsimp)
 apply (split option.splits, rule conjI, rule impI)
@@ -2127,31 +2060,31 @@
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q", simp)
+apply (case_tac "obj = D_msgq q", simp)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj_removemsgq dalive_simps split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q", simp)
+apply (case_tac "obj = D_msgq q", simp)
 apply (rule_tac x = obj' in exI)
 apply (frule_tac obj = obj' in co2sobj_smsgq_imp, erule exE)
-apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj_removemsgq dalive_simps split:t_dobject.splits if_splits)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+apply (simp add:co2sobj_removemsgq dalive_co2sobj_removemsgq)
 
 apply (rule impI)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q", simp)
+apply (case_tac "obj = D_msgq q", simp)
 apply (simp, rule conjI, rule_tac x = obj in exI)
-apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj_removemsgq dalive_simps split:t_dobject.splits if_splits)
 apply (rule notI, simp, frule_tac obj = obj in co2sobj_smsgq_imp, erule exE)
-apply (erule_tac x = obj in allE, simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+apply (erule_tac x = obj in allE, simp add:co2sobj_removemsgq dalive_co2sobj_removemsgq)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q", simp)
+apply (case_tac "obj = D_msgq q", simp)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+apply (simp add:co2sobj_removemsgq dalive_co2sobj_removemsgq)
 done
 
 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
@@ -2160,9 +2093,9 @@
   case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q, cp2sproc s p) of
     (Some sq, Some sq', Some sp) \<Rightarrow> if (O_msg q m \<in> tainted s \<and> O_proc p \<notin> tainted s)
                                     then update_s2ss_obj s (update_s2ss_obj s (s2ss s)
-                                                            (O_proc p) (S_proc sp False) (S_proc sp True))
-                                         (O_msgq q) (S_msgq sq) (S_msgq sq')
-                                    else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+                                                            (D_proc p) (S_proc sp False) (S_proc sp True))
+                                         (D_msgq q) (S_msgq sq) (S_msgq sq')
+                                    else update_s2ss_obj s (s2ss s) (D_msgq q) (S_msgq sq) (S_msgq sq')
   | _ \<Rightarrow> {})"
 apply (frule vt_grant_os, frule vd_cons)
 apply (case_tac "cq2smsgq s q")
@@ -2178,161 +2111,153 @@
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI2, rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, rule disjI2, simp)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (frule co2sobj_smsgq_imp, erule exE)
-apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (rule_tac x = "D_msgq qa" in exI, simp add:dalive_recvmsg co2sobj_recvmsg)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (frule co2sobj_sproc_imp, erule exE)
-apply (rule_tac x = "O_proc pa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (rule_tac x = "D_proc pa" in exI, simp add:dalive_recvmsg co2sobj_recvmsg)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI2,  simp add:co2sobj.simps cp2sproc_other)
 apply (rule notI, simp)
 apply (rule disjI2, simp, rule conjI, rule disjI2)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (rule notI, simp)
 apply (frule co2sobj_smsgq_imp, erule exE)
-apply (erule_tac x = "O_msgq qa" in allE, simp add:alive_recvmsg co2sobj_recvmsg split:if_splits)
+apply (erule_tac x = "D_msgq qa" in allE, simp add:dalive_recvmsg co2sobj_recvmsg split:if_splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*}, simp, erule disjE)
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (erule exE, erule conjE)
-apply (case_tac "obj = O_msgq q", simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_msgq q", simp add:co2sobj.simps)
+apply (case_tac "obj = D_proc p")
 apply (frule_tac co2sobj_sproc_imp, erule exE)
-apply (rule_tac x = "O_proc pa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (rule_tac x = "D_proc pa" in exI, simp add:dalive_recvmsg co2sobj_recvmsg)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI2, rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, rule disjI2, simp, rule conjI)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (rule notI, simp)
 apply (frule co2sobj_sproc_imp, erule exE)
-apply (erule_tac x = "O_proc pa" in allE, simp add:co2sobj_recvmsg split:t_object.splits)
+apply (erule_tac x = "D_proc pa" in allE, simp add:co2sobj_recvmsg split:t_dobject.splits)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (frule co2sobj_smsgq_imp, erule exE)
-apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (rule_tac x = "D_msgq qa" in exI, simp add:dalive_recvmsg co2sobj_recvmsg)
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (rule disjI2, simp, rule conjI)
 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)
 apply (rule notI, simp add:co2sobj.simps cp2sproc_other)
 apply (rule disjI2, simp, rule conjI, rule disjI2, rule conjI)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (rule notI, simp, frule co2sobj_sproc_imp, erule exE)
-apply (erule_tac x = "O_proc pa" in allE, simp add:co2sobj_recvmsg)
+apply (erule_tac x = "D_proc pa" in allE, simp add:co2sobj_recvmsg)
 apply (rule notI, simp, frule co2sobj_smsgq_imp, erule exE)
-apply (rotate_tac 12, erule_tac x = "O_msgq qa" in allE, simp add:co2sobj_recvmsg)
+apply (rotate_tac 12, erule_tac x = "D_msgq qa" in allE, simp add:co2sobj_recvmsg)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*}, simp)
 apply (tactic {*my_clarify_tac 1*})
-apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
+apply (rule_tac x = "D_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)
 apply (tactic {*my_clarify_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (simp add:co2sobj.simps)
-apply (case_tac "obj = O_proc p")
+apply (case_tac "obj = D_proc p")
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 
 apply (simp add:update_s2ss_obj_def)
 
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (frule co2sobj_smsgq_imp, erule exE)
-apply (rule_tac x = "O_msgq qa" in exI, simp add:alive_recvmsg co2sobj_recvmsg)
+apply (rule_tac x = "D_msgq qa" in exI, simp add:dalive_recvmsg co2sobj_recvmsg)
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 apply (simp add:co2sobj.simps)
 
 apply (tactic {*my_clarify_tac 1*})
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (rule disjI1, simp add:co2sobj.simps)
 apply (rule disjI2, simp, rule conjI)
 apply (rule_tac x = obj in exI)
-apply (simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)
+apply (simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)
 apply (simp add:co2sobj.simps)
 apply (rule notI, simp)
-apply (frule co2sobj_smsgq_imp, erule exE, erule_tac x = "O_msgq qa" in allE)
+apply (frule co2sobj_smsgq_imp, erule exE, erule_tac x = "D_msgq qa" in allE)
 apply (simp add:co2sobj_recvmsg)
 apply (tactic {*my_setiff_tac 1*})
-apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (rule_tac x = "D_msgq q" in exI, simp add:co2sobj.simps)
 apply (tactic {*my_setiff_tac 1*})
-apply (case_tac "obj = O_msgq q")
+apply (case_tac "obj = D_msgq q")
 apply (simp add:co2sobj.simps)
 apply (rule_tac x = obj in exI)
-apply (auto simp add:alive_recvmsg co2sobj_recvmsg split:t_object.splits if_splits)[1]
-apply (simp add:co2sobj.simps)
-apply (simp add:co2sobj.simps)
+apply (auto simp add:dalive_recvmsg co2sobj_recvmsg split:t_dobject.splits if_splits)[1]
 apply (simp add:co2sobj.simps)
 done
 

--- a/no_shm_selinux/S2ss_prop2.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/S2ss_prop2.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -14,11 +14,11 @@
 apply (rule_tac x = obj in exI)
 thm co2sobj_other
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_bind:
@@ -27,11 +27,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_connect:
@@ -40,11 +40,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_listen:
@@ -53,11 +53,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_accept:
@@ -66,11 +66,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_send:
@@ -79,11 +79,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_recv:
@@ -92,11 +92,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemma s2ss_shutdown:
@@ -105,11 +105,11 @@
 apply (tactic {*my_seteq_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (simp add:co2sobj_other)
-apply (simp add:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_other)
-apply (auto simp:co2sobj.simps alive_simps split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps dalive_simps split:t_object.splits if_splits)
 done
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open

--- a/no_shm_selinux/Static.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Static.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -99,38 +99,30 @@
      | _ \<Rightarrow> None)"
 *)
 
-fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
+fun init_obj2sobj :: "t_dobject \<Rightarrow> t_sobject option"
 where
-  "init_obj2sobj (O_proc p) = 
+  "init_obj2sobj (D_proc p) = 
      (case (init_cp2sproc p) of 
        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
      | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_file f) = 
+| "init_obj2sobj (D_file f) = 
      Some (S_file (init_cf2sfiles f) 
                   (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
-| "init_obj2sobj (O_dir f) = 
+| "init_obj2sobj (D_dir f) = 
      (case (init_cf2sfile f) of
            Some sf \<Rightarrow> Some (S_dir sf) 
          | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) = None"
-
-(*
-     (case (init_cq2smsgq q) of
-       Some sq \<Rightarrow> Some (S_msgq sq)
-     | _ \<Rightarrow> None)"
+| "init_obj2sobj (D_msgq q) = None"
 
-| "init_obj2sobj (O_shm h) = 
-     (case (init_ch2sshm h) of 
-       Some sh \<Rightarrow> Some (S_shm sh)
-     | _       \<Rightarrow> None)"  
-| "init_obj2sobj (O_msg q m) = 
-     (case (init_cq2smsgq q, init_cm2smsg q m) of 
-        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-      | _                  \<Rightarrow> None)" *)
-| "init_obj2sobj _ = None"
+fun init_dalive :: "t_dobject \<Rightarrow> bool"
+where
+  "init_dalive (D_proc p) = (p \<in> init_procs)"
+| "init_dalive (D_file f) = (is_init_file f)"
+| "init_dalive (D_dir  f) = (is_init_dir  f)"
+| "init_dalive (D_msgq q) = False"
 
 definition  
-  "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
+  "init_static_state \<equiv> {sobj. \<exists> obj. init_dalive obj \<and> init_obj2sobj obj = Some sobj}"
 
 (**************** translation from dynamic to static *******************)
 
@@ -227,39 +219,33 @@
                      (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
                    | _ \<Rightarrow> None)"
 
-fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
+fun co2sobj :: "t_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject option"
 where
-  "co2sobj s (O_proc p) = 
+  "co2sobj s (D_proc p) = 
      (case (cp2sproc s p) of 
         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
       | _       \<Rightarrow> None)"
-| "co2sobj s (O_file f) = 
+| "co2sobj s (D_file f) = 
      Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
-| "co2sobj s (O_dir f) = 
+| "co2sobj s (D_dir f) = 
      (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)
       | _ \<Rightarrow> None)"
-| "co2sobj s (O_msgq q) = 
+| "co2sobj s (D_msgq q) = 
      (case (cq2smsgq s q) of
         Some sq \<Rightarrow> Some (S_msgq sq)
       | _ \<Rightarrow> None)"
-(*
-| "co2sobj s (O_shm h) = 
-     (case (ch2sshm s h) of 
-        Some sh \<Rightarrow> Some (S_shm sh)
-      | _ \<Rightarrow> None)"
 
-| "co2sobj s (O_msg q m) = 
-     (case (cq2smsgq s q, cm2smsg s q m) of 
-       (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-     | _ \<Rightarrow> None)"
-*)
-| "co2sobj s _ = None"
-
+fun dalive :: "t_state \<Rightarrow> t_dobject \<Rightarrow> bool"
+where
+  "dalive s (D_proc p) = (p \<in> current_procs s)"
+| "dalive s (D_file f) = (is_file s f)"
+| "dalive s (D_dir  f) = (is_dir  s f)"
+| "dalive s (D_msgq q) = (q \<in> current_msgqs s)"
 
 definition s2ss :: "t_state \<Rightarrow> t_static_state"
 where
-  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
+  "s2ss s \<equiv> {sobj. \<exists> obj. dalive s obj \<and> co2sobj s obj = Some sobj}"
 
 
 (* ******************************************************** *)

--- a/no_shm_selinux/Static_type.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Static_type.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -95,4 +95,11 @@
  *)
 type_synonym t_static_state = "t_sobject set"
 
+(* dynamic objects that are traced by static world, so fd/msg are ignored *)
+datatype t_dobject = 
+  D_proc "t_process" 
+| D_file "t_file"
+| D_dir  "t_file"
+| D_msgq "t_msgq"
+
 end
\ No newline at end of file

--- a/no_shm_selinux/Temp.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Temp.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -14,9 +14,12 @@
 where
   "add_ss ss so \<equiv> ss \<union> {so}"
 
+(*
 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
 where
   "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"
+*)
+
 
 (* all reachable static states(sobjects set) *)
 inductive_set static :: "t_static_state set"