equal
deleted
inserted
replaced
23 "\<lbrakk>m \<noteq> hd (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
23 "\<lbrakk>m \<noteq> hd (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> |
24 \<Longrightarrow> (m \<in> set (tl (msgs_of_queue s q))) = (m \<in> set (msgs_of_queue s q))" |
24 \<Longrightarrow> (m \<in> set (tl (msgs_of_queue s q))) = (m \<in> set (msgs_of_queue s q))" |
25 apply (drule distinct_queue_msgs, simp) |
25 apply (drule distinct_queue_msgs, simp) |
26 apply (case_tac "msgs_of_queue s q", auto) |
26 apply (case_tac "msgs_of_queue s q", auto) |
27 done |
27 done |
28 |
|
29 lemma is_file_in_current: |
|
30 "is_file s f \<Longrightarrow> f \<in> current_files s" |
|
31 by (auto simp:is_file_def current_files_def split:option.splits) |
|
32 |
|
33 lemma is_dir_in_current: |
|
34 "is_dir s f \<Longrightarrow> f \<in> current_files s" |
|
35 by (auto simp:is_dir_def current_files_def split:option.splits) |
|
36 |
28 |
37 lemma is_tcp_in_current: |
29 lemma is_tcp_in_current: |
38 "is_tcp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>" |
30 "is_tcp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>" |
39 by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits) |
31 by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits) |
40 |
32 |