(*<*)
theory Current_prop
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
begin
(*>*)

context flask begin

lemma not_init_intro_proc:
  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
using not_deleted_init_proc by auto

lemma not_init_intro_proc':
  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
using not_deleted_init_proc by auto

lemma tobj_in_init_alive:
  "tobj_in_init obj \<Longrightarrow> init_alive obj"
by (case_tac obj, auto)

lemma tobj_in_alive:
  "tobj_in_init obj \<Longrightarrow> alive [] obj"
by (case_tac obj, auto simp:is_file_nil)

end

end