--- a/Alive_prop.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Alive_prop.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
 theory Alive_prop
-imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop
+imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_prop
 begin
 
 context flask begin
@@ -51,6 +51,8 @@
             dest:is_dir_in_current split:if_splits option.splits)
 done
 
+(* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant. 
+ * chunhan, 2013-11-20
 lemma alive_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
      \<lambda> obj. case obj of
@@ -68,6 +70,7 @@
 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
                  is_tcp_sock_simps is_udp_sock_simps
             dest:is_dir_in_current split:if_splits option.splits)
+
 done
 
 lemma alive_clone:
@@ -90,6 +93,48 @@
            intro:is_tcp_in_current is_udp_in_current
             dest:is_dir_in_current split:if_splits option.splits)
 done
+*)
+
+lemma alive_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
+     \<lambda> obj. case obj of
+              O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)
+                             else if (p = p') then False
+                                  else alive s (O_fd p' fd))
+            | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+                                      else alive s (O_tcp_sock (p', fd)))
+            | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+                                      else alive s (O_udp_sock (p', fd)))
+            | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
+                 is_tcp_sock_simps is_udp_sock_simps
+            dest:is_dir_in_current split:if_splits option.splits)
+apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto)
+
+done
+
+lemma alive_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = (
+     \<lambda> obj. case obj of
+              O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj
+            | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
+                             else if (p'' = p') then False
+                                  else alive s obj
+            | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
+                                      else if (p'' = p') then False
+                                           else alive s (O_tcp_sock (p'', fd)))
+            | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
+                                      else if (p'' = p') then False
+                                           else alive s (O_udp_sock (p'', fd)))
+            | _ \<Rightarrow> alive s obj )"  
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
+                 is_tcp_sock_simps is_udp_sock_simps
+           intro:is_tcp_in_current is_udp_in_current
+            dest:is_dir_in_current split:if_splits option.splits)
+done
+
 
 lemma alive_kill:
   "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (