diff -r 002c34a6ff4f -r db0e8601c229 Alive_prop.thy
--- a/Alive_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Alive_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -109,9 +109,8 @@
 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)
-
+            dest:is_dir_in_current split:if_splits option.splits
+  dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
 done
 
 lemma alive_clone:
@@ -121,21 +120,19 @@
             | 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)))
+            | 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
            intro:is_tcp_in_current is_udp_in_current
-            dest:is_dir_in_current split:if_splits option.splits)
+            dest:is_dir_in_current split:if_splits option.splits
+  dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
 done
 
-
 lemma alive_kill:
   "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
      \<lambda> obj. case obj of