88 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
88 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
89 |
89 |
90 lemma is_dir_nil: "is_dir [] = is_init_dir" |
90 lemma is_dir_nil: "is_dir [] = is_init_dir" |
91 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) |
91 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) |
92 |
92 |
|
93 lemma is_udp_sock_nil: |
|
94 "is_udp_sock [] k = is_init_udp_sock k" |
|
95 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits) |
|
96 |
93 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)" |
97 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)" |
94 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
98 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
95 dest:init_socket_has_inode split:option.splits) |
99 dest:init_socket_has_inode split:option.splits) |
96 done |
100 done |
97 |
101 |
98 lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))" |
102 lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))" |
99 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
103 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
100 dest:init_socket_has_inode split:option.splits) |
104 dest:init_socket_has_inode split:option.splits) |
101 done |
105 done |
102 |
106 |
103 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 |
107 lemma is_init_udp_sock_prop3: |
|
108 "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
|
109 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits |
|
110 dest:init_socket_has_inode inos_has_sock_tag) |
|
111 |
|
112 lemma is_init_udp_sock_prop4: |
|
113 "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 |
|
115 dest:init_socket_has_inode inos_has_sock_tag) |
|
116 |
|
117 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 |
|
119 |
|
120 lemma is_tcp_sock_nil: |
|
121 "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) |
104 |
123 |
105 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)" |
124 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)" |
106 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
125 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
107 dest:init_socket_has_inode split:option.splits) |
126 dest:init_socket_has_inode split:option.splits) |
108 done |
127 done |
110 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))" |
129 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))" |
111 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
130 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
112 dest:init_socket_has_inode split:option.splits) |
131 dest:init_socket_has_inode split:option.splits) |
113 done |
132 done |
114 |
133 |
115 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 |
134 lemma is_init_tcp_sock_prop3: |
116 |
135 "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
|
136 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits |
|
137 dest:init_socket_has_inode inos_has_sock_tag) |
|
138 |
|
139 lemma is_init_tcp_sock_prop4: |
|
140 "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 |
|
142 dest:init_socket_has_inode inos_has_sock_tag) |
|
143 |
|
144 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 |
117 |
146 |
118 lemma init_parent_file_prop1: |
147 lemma init_parent_file_prop1: |
119 "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf" |
148 "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf" |
120 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3) |
149 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3) |
121 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+) |
150 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+) |