theory Delete_prop
imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop
begin

context flask begin

lemma died_cons_I: "died obj s \<Longrightarrow> died obj (e # s)"
by (case_tac e, auto)

lemma not_died_cons_D: "\<not> died obj (e # s) \<Longrightarrow> \<not> died obj s" 
by (auto dest:died_cons_I)

lemma cons_app_simp_aux:
  "(a # b) @ c = a # (b @ c)" by auto

lemma not_died_app_I:
  "died obj s \<Longrightarrow> died obj (s' @ s)"
apply (induct s', simp)
by (simp add:cons_app_simp_aux died_cons_I)

lemma not_died_app_D:
  "\<not> died obj (s' @ s) \<Longrightarrow> \<not> died obj s"
apply (rule notI)
by (simp add:not_died_app_I)

lemma not_died_init_file:
  "\<lbrakk>\<not> died (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
apply (induct s, simp add:is_file_nil)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a) prefer 6 apply (case_tac option)
apply (auto simp:is_file_simps split:option.splits)
done

lemma not_died_init_dir:
  "\<lbrakk>\<not> died (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"
apply (induct s, simp add:is_dir_nil)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a) prefer 6 apply (case_tac option)
apply (auto simp:is_dir_simps split:option.splits)
done

lemma not_died_init_proc:
  "\<lbrakk>\<not> died (O_proc p) s; p \<in> init_procs\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
apply (induct s, simp)
by (case_tac a, auto)

lemma current_fd_imp_current_proc:
  "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
apply (induct s)
apply (simp add:init_fds_of_proc_prop1)
apply (frule vd_cons, drule vt_grant_os, case_tac a)
by (auto split:if_splits option.splits)

lemma not_died_init_fd_aux:
  "\<lbrakk>\<not> died (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> 
   \<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> died (O_proc p) s"
apply (induct s arbitrary: p, simp)
apply (frule vd_cons, drule vt_grant_os)
apply (case_tac a, auto dest:current_fd_imp_current_proc)
done

lemma not_died_init_fd2:
  "\<lbrakk>\<not> died (O_fd p fd) s; fd \<in> init_fds_of_proc p; valid s\<rbrakk> \<Longrightarrow> \<not> died (O_proc p) s"
by (auto dest:not_died_init_fd_aux)

lemma not_died_init_fd1:
  "\<lbrakk>\<not> died (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
by (auto dest:not_died_init_fd_aux)

lemma not_died_init_tcp_aux:
  "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> died (O_proc p) s"
apply (induct s arbitrary:p, simp add:is_tcp_sock_nil)
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_died_init_tcp1:
  "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> is_tcp_sock s (p,fd)"
by (auto dest:not_died_init_tcp_aux)

lemma not_died_init_tcp2:
  "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> \<not> died (O_proc p) s"
by (auto dest:not_died_init_tcp_aux)

lemma not_died_init_udp_aux:
  "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> died (O_proc p) s"
apply (induct s arbitrary:p, simp add:is_udp_sock_nil)
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_died_init_udp1:
  "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> is_udp_sock s (p,fd)"
by (auto dest:not_died_init_udp_aux)

lemma not_died_init_udp2:
  "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
   \<Longrightarrow> \<not> died (O_proc p) s"
by (auto dest:not_died_init_udp_aux)

(*
lemma not_died_init_shm:
  "\<lbrakk>\<not> died (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
apply (induct s, simp)
by (case_tac a, auto)
*)

(*
lemma not_died_init_msgq:
  "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
apply (induct s, simp)
by (case_tac a, auto)
*)

lemma current_msg_imp_current_msgq:
  "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
apply (induct s, simp)
apply (frule vd_cons, drule vt_grant_os)
apply (case_tac a, auto split:if_splits)
done

(*
lemma not_died_init_msg:
  "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"
apply (induct s, simp)
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 q", simp+)
done
*)

lemma not_died_imp_alive: (* init_alive obj;  *)
  "\<lbrakk>\<not> died obj s;  valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
apply (case_tac obj)
apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc
   not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 
  (* not_died_init_shm not_died_init_msg not_died_init_msgq*) 
           intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current
  current_msg_imp_current_msgq)
done

lemma not_died_cur_file_app:
  "\<lbrakk>\<not> died (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_died_cur_dir_app:
  "\<lbrakk>\<not> died (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_died_cur_proc_app:
  "\<lbrakk>\<not> died (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_died_cur_fd_app:
  "\<lbrakk>\<not> died (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_died_cur_tcp_app:
  "\<lbrakk>\<not> died (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_died_cur_udp_app:
  "\<lbrakk>\<not> died (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_died_cur_shm_app:
  "\<lbrakk>\<not> died (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_died_cur_msgq_app:
  "\<lbrakk>\<not> died (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_died_cur_msg_app:
  "\<lbrakk>\<not> died (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_died_imp_alive_app:
  "\<lbrakk>\<not> died obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj"
apply (case_tac obj)
apply (auto dest!: not_died_cur_file_app not_died_cur_dir_app
  not_died_cur_proc_app not_died_cur_fd_app not_died_cur_tcp_app not_died_cur_msg_app
  not_died_cur_udp_app  (* not_died_cur_shm_app *) not_died_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

lemma not_died_imp_alive_cons:
  "\<lbrakk>\<not> died obj (e # s); valid (e # s); alive s obj\<rbrakk> \<Longrightarrow> alive (e # s) obj"
using not_died_imp_alive_app[where s = s and s' = "[e]" and obj = obj] 
by auto

end

context tainting begin

lemma deleted_died:
  "appropriate obj \<Longrightarrow> died obj s = (deleted obj s \<or> exited obj s)"
apply (induct s)
apply (simp, case_tac obj, simp+)
apply (case_tac a, case_tac [!] obj, auto)
done

end

(*

lemma nodel_imp_un_died:
  "no_del_event s \<Longrightarrow> \<not> died obj s"
by (induct s, simp, case_tac a,auto)

lemma nodel_exists_remains:
  "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"
apply (drule_tac obj = obj in nodel_imp_un_died)
by (simp add:not_died_imp_exists')

lemma nodel_imp_exists:
  "\<lbrakk>no_del_event s; exists [] obj\<rbrakk> \<Longrightarrow> exists s obj"
apply (drule_tac obj = obj in nodel_imp_un_died)
by (simp add:not_died_imp_exists)

lemma no_del_event_cons_D:
  "no_del_event (e # s) \<Longrightarrow> no_del_event s"
by (case_tac e, auto)
*)

end