43 by (auto simp:proc_fd_of_file_def) |
43 by (auto simp:proc_fd_of_file_def) |
44 |
44 |
45 lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
45 lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
46 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur') |
46 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur') |
47 |
47 |
|
48 lemma file_fds_subset_pfds: |
|
49 "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p" |
|
50 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds) |
|
51 |
|
52 lemma tcp_filefd_conflict: |
|
53 "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False" |
|
54 apply (induct s, simp) |
|
55 apply (auto simp:is_tcp_sock_simps) |
|
56 |
|
57 |
|
58 lemma tcp_not_file_fd: |
|
59 "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
|
60 apply (auto simp:proc_file_fds_def) |
|
61 |
|
62 lemma udp_not_file_fd: |
|
63 "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
|
64 |
|
65 lemma |
48 |
66 |
49 (******************* rebuild proc_fd_of_file simpset ***********************) |
67 (******************* rebuild proc_fd_of_file simpset ***********************) |
50 (* |
68 (* |
51 lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> |
69 lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> |
52 proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')" |
70 proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')" |