--- a/Delete_prop.thy	Thu May 09 11:19:44 2013 +0800
+++ b/Delete_prop.thy	Fri May 10 10:23:34 2013 +0800
@@ -10,6 +10,19 @@
 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" 
 by (auto dest:deleted_cons_I)
 
+lemma cons_app_simp_aux:
+  "(a # b) @ c = a # (b @ c)" by auto
+
+lemma not_deleted_app_I:
+  "deleted obj s \<Longrightarrow> deleted obj (s' @ s)"
+apply (induct s', simp)
+by (simp add:cons_app_simp_aux deleted_cons_I)
+
+lemma not_deleted_app_D:
+  "\<not> deleted obj (s' @ s) \<Longrightarrow> \<not> deleted obj s"
+apply (rule notI)
+by (simp add:not_deleted_app_I)
+
 lemma not_deleted_init_file:
   "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
 apply (induct s, simp add:is_init_file_prop1)
@@ -129,14 +142,80 @@
   current_msg_imp_current_msgq)
 done
 
-lemma cons_app_simp_aux:
-  "(a # b) @ c = a # (b @ c)" by auto
+lemma not_deleted_cur_file_app:
+  "\<lbrakk>\<not> deleted (O_file f) (s' @ s); valid (s' @ s); is_file s f\<rbrakk> \<Longrightarrow> is_file (s' @ s) f"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, frule vt_grant_os, simp)
+apply (case_tac a) prefer 6 apply (case_tac option)
+apply (auto simp:is_file_simps split:option.splits)
+done
+
+lemma not_deleted_cur_dir_app:
+  "\<lbrakk>\<not> deleted (O_dir f) (s' @ s); valid (s' @ s); is_dir s f\<rbrakk> \<Longrightarrow> is_dir (s' @ s) f"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, frule vt_grant_os, simp)
+apply (case_tac a) prefer 6 apply (case_tac option)
+apply (auto simp:is_dir_simps split:option.splits)
+done
+
+lemma not_deleted_cur_proc_app:
+  "\<lbrakk>\<not> deleted (O_proc p) (s' @ s); p \<in> current_procs s\<rbrakk> \<Longrightarrow> p \<in> current_procs (s' @ s)"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+by (case_tac a, auto)
+
+lemma not_deleted_cur_fd_app:
+  "\<lbrakk>\<not> deleted (O_fd p fd) (s' @ s); valid (s' @ s); fd \<in> current_proc_fds s p\<rbrakk> 
+   \<Longrightarrow> fd \<in> current_proc_fds (s' @ s) p"
+apply (induct s' arbitrary: p, simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, drule vt_grant_os)
+apply (case_tac a, auto dest:current_fd_imp_current_proc)
+done
+
+lemma not_deleted_cur_tcp_app:
+  "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) (s' @ s); valid (s' @ s); is_tcp_sock s (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_tcp_sock (s' @ s) (p,fd)"
+apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 
+         dest:is_tcp_sock_imp_curernt_proc)
+
+lemma not_deleted_cur_udp_app:
+  "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) (s' @ s); valid (s' @ s); is_udp_sock s (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_udp_sock (s' @ s) (p,fd)"
+apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 
+         dest:is_udp_sock_imp_curernt_proc)
+
+lemma not_deleted_cur_shm_app:
+  "\<lbrakk>\<not> deleted (O_shm h) (s' @ s); h \<in> current_shms s\<rbrakk> \<Longrightarrow> h \<in> current_shms (s' @ s)"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+by (case_tac a, auto)
+
+lemma not_deleted_cur_msgq_app:
+  "\<lbrakk>\<not> deleted (O_msgq q) (s' @ s); q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (s' @ s)"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+by (case_tac a, auto)
+
+lemma not_deleted_cur_msg_app:
+  "\<lbrakk>\<not> deleted (O_msg q m) (s' @ s); valid (s' @ s); m \<in> set (msgs_of_queue s q)\<rbrakk> 
+   \<Longrightarrow> m \<in> set (msgs_of_queue (s' @ s) q)"
+apply (induct s', simp, simp add:cons_app_simp_aux)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto dest:current_msg_imp_current_msgq)
+apply (case_tac "msgs_of_queue (s' @ s) q", simp+)
+done
 
 lemma not_deleted_imp_alive_app:
-  "\<lbrakk>\<not> deleted obj (s'@s); alive s obj\<rbrakk> \<Longrightarrow> alive (s'@s) obj"
-apply (induct s', simp, simp only:cons_app_simp_aux)
-apply (frule not_deleted_cons_D, simp)
-apply (case_tac a, case_tac [!] obj, auto)
+  "\<lbrakk>\<not> deleted obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj"
+apply (case_tac obj)
+apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app
+  not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app 
+  not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app
+           intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 
+  current_msg_imp_current_msgq)
 done
 
 (*