132 lemma cons_app_simp_aux:

   145 lemma not_deleted_cur_file_app:

   133   "(a # b) @ c = a # (b @ c)" by auto

   146   "\<lbrakk>\<not> deleted (O_file f) (s' @ s); valid (s' @ s); is_file s f\<rbrakk> \<Longrightarrow> is_file (s' @ s) f"

   147 apply (induct s', simp, simp add:cons_app_simp_aux)

   148 apply (frule vd_cons, frule vt_grant_os, simp)

   149 apply (case_tac a) prefer 6 apply (case_tac option)

   150 apply (auto simp:is_file_simps split:option.splits)

   151 done

   152 

   153 lemma not_deleted_cur_dir_app:

   154   "\<lbrakk>\<not> deleted (O_dir f) (s' @ s); valid (s' @ s); is_dir s f\<rbrakk> \<Longrightarrow> is_dir (s' @ s) f"

   155 apply (induct s', simp, simp add:cons_app_simp_aux)

   156 apply (frule vd_cons, frule vt_grant_os, simp)

   157 apply (case_tac a) prefer 6 apply (case_tac option)

   158 apply (auto simp:is_dir_simps split:option.splits)

   159 done

   160 

   161 lemma not_deleted_cur_proc_app:

   162   "\<lbrakk>\<not> deleted (O_proc p) (s' @ s); p \<in> current_procs s\<rbrakk> \<Longrightarrow> p \<in> current_procs (s' @ s)"

   163 apply (induct s', simp, simp add:cons_app_simp_aux)

   164 by (case_tac a, auto)

   165 

   166 lemma not_deleted_cur_fd_app:

   167   "\<lbrakk>\<not> deleted (O_fd p fd) (s' @ s); valid (s' @ s); fd \<in> current_proc_fds s p\<rbrakk> 

   168    \<Longrightarrow> fd \<in> current_proc_fds (s' @ s) p"

   169 apply (induct s' arbitrary: p, simp, simp add:cons_app_simp_aux)

   170 apply (frule vd_cons, drule vt_grant_os)

   171 apply (case_tac a, auto dest:current_fd_imp_current_proc)

   172 done

   173 

   174 lemma not_deleted_cur_tcp_app:

   175   "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) (s' @ s); valid (s' @ s); is_tcp_sock s (p,fd)\<rbrakk> 

   176    \<Longrightarrow> is_tcp_sock (s' @ s) (p,fd)"

   177 apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)

   178 apply (frule vd_cons, frule vt_grant_os)

   179 apply (case_tac a) prefer 6 apply (case_tac option)

   180 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 

   181          dest:is_tcp_sock_imp_curernt_proc)

   182 

   183 lemma not_deleted_cur_udp_app:

   184   "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) (s' @ s); valid (s' @ s); is_udp_sock s (p,fd)\<rbrakk> 

   185    \<Longrightarrow> is_udp_sock (s' @ s) (p,fd)"

   186 apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)

   187 apply (frule vd_cons, frule vt_grant_os)

   188 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 

   190          dest:is_udp_sock_imp_curernt_proc)

   191 

   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:

   198   "\<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)

   200 by (case_tac a, auto)

   201 

   202 lemma not_deleted_cur_msg_app:

   203   "\<lbrakk>\<not> deleted (O_msg q m) (s' @ s); valid (s' @ s); m \<in> set (msgs_of_queue s q)\<rbrakk> 

   204    \<Longrightarrow> m \<in> set (msgs_of_queue (s' @ s) q)"

   205 apply (induct s', simp, simp add:cons_app_simp_aux)

   206 apply (frule vd_cons, frule vt_grant_os)

   207 apply (case_tac a, auto dest:current_msg_imp_current_msgq)

   208 apply (case_tac "msgs_of_queue (s' @ s) q", simp+)

   209 done

   136   "\<lbrakk>\<not> deleted obj (s'@s); alive s obj\<rbrakk> \<Longrightarrow> alive (s'@s) obj"

   212   "\<lbrakk>\<not> deleted obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj"

   137 apply (induct s', simp, simp only:cons_app_simp_aux)

   213 apply (case_tac obj)

   138 apply (frule not_deleted_cons_D, simp)

   214 apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app

   139 apply (case_tac a, case_tac [!] obj, auto)

   215   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

   217            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 

   218   current_msg_imp_current_msgq)