equal
deleted
inserted
replaced
104 lemma not_deleted_init_udp2: |
104 lemma not_deleted_init_udp2: |
105 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
105 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
106 \<Longrightarrow> \<not> deleted (O_proc p) s" |
106 \<Longrightarrow> \<not> deleted (O_proc p) s" |
107 by (auto dest:not_deleted_init_udp_aux) |
107 by (auto dest:not_deleted_init_udp_aux) |
108 |
108 |
109 lemma not_deleted_init_shm: |
|
110 "\<lbrakk>\<not> deleted (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
|
111 apply (induct s, simp) |
|
112 by (case_tac a, auto) |
|
113 |
|
114 lemma not_deleted_init_msgq: |
109 lemma not_deleted_init_msgq: |
115 "\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
110 "\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
116 apply (induct s, simp) |
111 apply (induct s, simp) |
117 by (case_tac a, auto) |
112 by (case_tac a, auto) |
118 |
113 |
134 |
129 |
135 lemma not_deleted_imp_alive: |
130 lemma not_deleted_imp_alive: |
136 "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
131 "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
137 apply (case_tac obj) |
132 apply (case_tac obj) |
138 apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc |
133 apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc |
139 not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm |
134 not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 |
140 not_deleted_init_msgq |
135 not_deleted_init_msgq |
141 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
136 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
142 current_msg_imp_current_msgq) |
137 current_msg_imp_current_msgq) |
143 done |
138 done |
144 |
139 |
187 apply (frule vd_cons, frule vt_grant_os) |
182 apply (frule vd_cons, frule vt_grant_os) |
188 apply (case_tac a) prefer 6 apply (case_tac option) |
183 apply (case_tac a) prefer 6 apply (case_tac option) |
189 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits |
184 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits |
190 dest:is_udp_sock_imp_curernt_proc) |
185 dest:is_udp_sock_imp_curernt_proc) |
191 |
186 |
192 lemma not_deleted_cur_shm_app: |
|
193 "\<lbrakk>\<not> deleted (O_shm h) (s' @ s); h \<in> current_shms s\<rbrakk> \<Longrightarrow> h \<in> current_shms (s' @ s)" |
|
194 apply (induct s', simp, simp add:cons_app_simp_aux) |
|
195 by (case_tac a, auto) |
|
196 |
|
197 lemma not_deleted_cur_msgq_app: |
187 lemma not_deleted_cur_msgq_app: |
198 "\<lbrakk>\<not> deleted (O_msgq q) (s' @ s); q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (s' @ s)" |
188 "\<lbrakk>\<not> deleted (O_msgq q) (s' @ s); q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (s' @ s)" |
199 apply (induct s', simp, simp add:cons_app_simp_aux) |
189 apply (induct s', simp, simp add:cons_app_simp_aux) |
200 by (case_tac a, auto) |
190 by (case_tac a, auto) |
201 |
191 |
211 lemma not_deleted_imp_alive_app: |
201 lemma not_deleted_imp_alive_app: |
212 "\<lbrakk>\<not> deleted obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj" |
202 "\<lbrakk>\<not> deleted obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj" |
213 apply (case_tac obj) |
203 apply (case_tac obj) |
214 apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app |
204 apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app |
215 not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app |
205 not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app |
216 not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app |
206 not_deleted_cur_udp_app not_deleted_cur_msgq_app |
217 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
207 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
218 current_msg_imp_current_msgq) |
208 current_msg_imp_current_msgq) |
219 done |
209 done |
220 |
210 |
221 lemma not_deleted_imp_alive_cons: |
211 lemma not_deleted_imp_alive_cons: |