64 apply (simp add:current_sockets_def, rule iffI) |
64 apply (simp add:current_sockets_def, rule iffI) |
65 using init_sockets_prop4 inos_has_sock_tag apply auto |
65 using init_sockets_prop4 inos_has_sock_tag apply auto |
66 apply (case_tac s, auto) |
66 apply (case_tac s, auto) |
67 done |
67 done |
68 |
68 |
|
69 lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None" |
|
70 by (auto dest: init_socket_has_inode) |
|
71 |
69 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5 |
72 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5 |
70 |
73 |
71 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files" |
74 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files" |
72 by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits) |
75 by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits) |
73 |
76 |
112 lemma is_init_udp_sock_prop4: |
115 lemma is_init_udp_sock_prop4: |
113 "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p" |
116 "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p" |
114 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits |
117 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits |
115 dest:init_socket_has_inode inos_has_sock_tag) |
118 dest:init_socket_has_inode inos_has_sock_tag) |
116 |
119 |
|
120 lemma is_init_udp_sock_prop5: |
|
121 "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None" |
|
122 by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6) |
|
123 |
117 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3 |
124 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3 |
118 is_init_udp_sock_prop4 |
125 is_init_udp_sock_prop4 is_init_udp_sock_prop5 |
119 |
126 |
120 lemma is_tcp_sock_nil: |
127 lemma is_tcp_sock_nil: |
121 "is_tcp_sock [] k = is_init_tcp_sock k" |
128 "is_tcp_sock [] k = is_init_tcp_sock k" |
122 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) |
129 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) |
123 |
130 |
139 lemma is_init_tcp_sock_prop4: |
146 lemma is_init_tcp_sock_prop4: |
140 "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p" |
147 "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p" |
141 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits |
148 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits |
142 dest:init_socket_has_inode inos_has_sock_tag) |
149 dest:init_socket_has_inode inos_has_sock_tag) |
143 |
150 |
|
151 lemma is_init_tcp_sock_prop5: |
|
152 "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None" |
|
153 by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6) |
|
154 |
144 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3 |
155 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3 |
145 is_init_tcp_sock_prop4 |
156 is_init_tcp_sock_prop4 is_init_tcp_sock_prop5 |
146 |
157 |
147 lemma init_parent_file_prop1: |
158 lemma init_parent_file_prop1: |
148 "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf" |
159 "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf" |
149 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3) |
160 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3) |
150 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+) |
161 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+) |
219 by (auto dest:init_filefd_valid) |
230 by (auto dest:init_filefd_valid) |
220 |
231 |
221 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f" |
232 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f" |
222 by (auto dest:init_filefd_valid simp:is_init_file_def) |
233 by (auto dest:init_filefd_valid simp:is_init_file_def) |
223 |
234 |
224 lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5 |
235 lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)" |
|
236 by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1) |
|
237 |
|
238 lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)" |
|
239 by (auto dest!:init_filefd_valid is_init_udp_sock_prop1) |
|
240 |
|
241 lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets" |
|
242 by (auto dest!:init_filefd_valid) |
|
243 |
|
244 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 |
225 |
245 |
226 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs" |
246 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs" |
227 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props) |
247 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props) |
228 |
248 |
229 lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p" |
249 lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p" |