(*<*)

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