23 apply (rule notI) |
23 apply (rule notI) |
24 by (simp add:not_deleted_app_I) |
24 by (simp add:not_deleted_app_I) |
25 |
25 |
26 lemma not_deleted_init_file: |
26 lemma not_deleted_init_file: |
27 "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f" |
27 "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f" |
28 apply (induct s, simp add:is_init_file_prop1) |
28 apply (induct s, simp add:is_file_nil) |
29 apply (frule vd_cons, frule vt_grant_os) |
29 apply (frule vd_cons, frule vt_grant_os) |
30 apply (case_tac a) prefer 6 apply (case_tac option) |
30 apply (case_tac a) prefer 6 apply (case_tac option) |
31 apply (auto simp:is_file_simps split:option.splits) |
31 apply (auto simp:is_file_simps split:option.splits) |
32 done |
32 done |
33 |
33 |
34 lemma not_deleted_init_dir: |
34 lemma not_deleted_init_dir: |
35 "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f" |
35 "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f" |
36 apply (induct s, simp add:is_init_dir_prop1) |
36 apply (induct s, simp add:is_dir_nil) |
37 apply (frule vd_cons, frule vt_grant_os) |
37 apply (frule vd_cons, frule vt_grant_os) |
38 apply (case_tac a) prefer 6 apply (case_tac option) |
38 apply (case_tac a) prefer 6 apply (case_tac option) |
39 apply (auto simp:is_dir_simps split:option.splits) |
39 apply (auto simp:is_dir_simps split:option.splits) |
40 done |
40 done |
41 |
41 |
69 by (auto dest:not_deleted_init_fd_aux) |
69 by (auto dest:not_deleted_init_fd_aux) |
70 |
70 |
71 lemma not_deleted_init_tcp_aux: |
71 lemma not_deleted_init_tcp_aux: |
72 "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> |
72 "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> |
73 \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
73 \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
74 apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1) |
74 apply (induct s arbitrary:p, simp add:is_tcp_sock_nil) |
75 apply (frule vd_cons, frule vt_grant_os) |
75 apply (frule vd_cons, frule vt_grant_os) |
76 apply (case_tac a) prefer 6 apply (case_tac option) |
76 apply (case_tac a) prefer 6 apply (case_tac option) |
77 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits |
77 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits |
78 dest:is_tcp_sock_imp_curernt_proc) |
78 dest:is_tcp_sock_imp_curernt_proc) |
79 |
79 |
88 by (auto dest:not_deleted_init_tcp_aux) |
88 by (auto dest:not_deleted_init_tcp_aux) |
89 |
89 |
90 lemma not_deleted_init_udp_aux: |
90 lemma not_deleted_init_udp_aux: |
91 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
91 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
92 \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
92 \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
93 apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1) |
93 apply (induct s arbitrary:p, simp add:is_udp_sock_nil) |
94 apply (frule vd_cons, frule vt_grant_os) |
94 apply (frule vd_cons, frule vt_grant_os) |
95 apply (case_tac a) prefer 6 apply (case_tac option) |
95 apply (case_tac a) prefer 6 apply (case_tac option) |
96 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits |
96 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits |
97 dest:is_udp_sock_imp_curernt_proc) |
97 dest:is_udp_sock_imp_curernt_proc) |
98 |
98 |