--- 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)