--- a/Current_sockets_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Current_sockets_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -242,6 +242,21 @@
 apply (case_tac t_sock_trans_state, case_tac [!] how)
 by auto
 
+lemma is_tcp_sock_imp_curernt_proc:
+  "\<lbrakk>is_tcp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+lemma is_udp_sock_imp_curernt_proc:
+  "\<lbrakk>is_udp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+
 (***** below should be adjusted after starting static analysis of sockets ! ??? ****)
 
 (*