diff -r 002c34a6ff4f -r db0e8601c229 Init_prop.thy
--- a/Init_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Init_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -66,6 +66,9 @@
 apply (case_tac s, auto)
 done
 
+lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest: init_socket_has_inode)
+
 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
 
 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"
@@ -114,8 +117,12 @@
 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
          dest:init_socket_has_inode inos_has_sock_tag)
 
+lemma is_init_udp_sock_prop5:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6)
+
 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3
-  is_init_udp_sock_prop4
+  is_init_udp_sock_prop4 is_init_udp_sock_prop5
 
 lemma is_tcp_sock_nil:
   "is_tcp_sock [] k = is_init_tcp_sock k"
@@ -141,8 +148,12 @@
 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
          dest:init_socket_has_inode inos_has_sock_tag)
 
+lemma is_init_tcp_sock_prop5:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6)
+
 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3
-  is_init_tcp_sock_prop4
+  is_init_tcp_sock_prop4 is_init_tcp_sock_prop5
 
 lemma init_parent_file_prop1: 
   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"
@@ -221,7 +232,16 @@
 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"
 by (auto dest:init_filefd_valid simp:is_init_file_def)
 
-lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5
+lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1)
+
+lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_udp_sock_prop1)
+
+lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets"
+by (auto dest!:init_filefd_valid)
+
+lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5 init_filefd_prop6 init_filefd_prop7 init_filefd_prop8
 
 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"
 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)