240 apply (case_tac "socket_state \<tau> s", simp add:socket_in_trans_def, case_tac a) |
240 apply (case_tac "socket_state \<tau> s", simp add:socket_in_trans_def, case_tac a) |
241 apply (auto simp:update_with_shuthow.simps socket_in_trans_def split:option.splits) |
241 apply (auto simp:update_with_shuthow.simps socket_in_trans_def split:option.splits) |
242 apply (case_tac t_sock_trans_state, case_tac [!] how) |
242 apply (case_tac t_sock_trans_state, case_tac [!] how) |
243 by auto |
243 by auto |
244 |
244 |
|
245 lemma is_tcp_sock_imp_curernt_proc: |
|
246 "\<lbrakk>is_tcp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
247 apply (induct s) |
|
248 apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3) |
|
249 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
250 by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits) |
|
251 |
|
252 lemma is_udp_sock_imp_curernt_proc: |
|
253 "\<lbrakk>is_udp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
254 apply (induct s) |
|
255 apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3) |
|
256 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
257 by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits) |
|
258 |
|
259 |
245 (***** below should be adjusted after starting static analysis of sockets ! ??? ****) |
260 (***** below should be adjusted after starting static analysis of sockets ! ??? ****) |
246 |
261 |
247 (* |
262 (* |
248 lemma cn_has_sockstate: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> socket_state \<tau> (p, fd) \<noteq> None" |
263 lemma cn_has_sockstate: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> socket_state \<tau> (p, fd) \<noteq> None" |
249 apply (induct \<tau> arbitrary: p) using init_socket_has_state |
264 apply (induct \<tau> arbitrary: p) using init_socket_has_state |