--- a/Proc_fd_of_file_prop.thy	Wed Nov 20 13:44:32 2013 +0800
+++ b/Proc_fd_of_file_prop.thy	Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
 theory Proc_fd_of_file_prop
-imports Main Flask Flask_type Valid_prop Current_files_prop
+imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop
 begin
 
 context flask begin
@@ -45,6 +45,24 @@
 lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')
 
+lemma file_fds_subset_pfds:
+  "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 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)
+
+lemma udp_not_file_fd:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+
+lemma
 
 (******************* rebuild proc_fd_of_file simpset ***********************)
 (*