--- a/Init_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Init_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -90,6 +90,10 @@
 lemma is_dir_nil: "is_dir [] = is_init_dir"
 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
 
+lemma is_udp_sock_nil:
+  "is_udp_sock [] k = is_init_udp_sock k"
+by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits)
+
 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
@@ -100,7 +104,22 @@
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2
+lemma is_init_udp_sock_prop3:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+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_prop4:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+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
+
+lemma is_tcp_sock_nil:
+  "is_tcp_sock [] k = is_init_tcp_sock k"
+by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits)
 
 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"
 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
@@ -112,8 +131,18 @@
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2
+lemma is_init_tcp_sock_prop3:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+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_prop4:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+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
 
 lemma init_parent_file_prop1: 
   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"