--- a/Proc_fd_of_file_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Proc_fd_of_file_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -49,20 +49,42 @@
   "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"
 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)
 
-lemma tcp_filefd_conflict:
-  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False"
-apply (induct s, simp)
-apply (auto simp:is_tcp_sock_simps)
+lemma filefd_socket_conflict:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; (p, fd) \<in> current_sockets s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s arbitrary:p)
+apply (simp add:current_sockets_simps init_filefd_prop8)
+apply (frule vt_grant_os, frule vd_cons, frule file_fds_subset_pfds, case_tac a)
+apply (auto simp:current_sockets_simps split:if_splits option.splits 
+            dest:cn_in_curp cn_in_curfd proc_fd_in_fds)
+done
 
+lemma is_tcp_in_current: "is_tcp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)
+
+lemma is_udp_in_current: "is_udp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)
 
 lemma tcp_not_file_fd:
-  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
-apply (auto simp:proc_file_fds_def)
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_tcp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
 
 lemma udp_not_file_fd:
-  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_udp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
 
-lemma
+lemma tcp_notin_file_fds:
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:tcp_not_file_fd)
+
+lemma udp_notin_file_fds:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:udp_not_file_fd)
 
 (******************* rebuild proc_fd_of_file simpset ***********************)
 (*