theory Current_prop

imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop

begin

(*<*)

context flask begin

lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"

apply (induct s arbitrary:p_flag)

apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac a, auto split:if_splits option.splits)

done

lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

apply (induct s arbitrary:p flag)

apply (simp, drule init_procs_has_shm, simp)

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac a, auto split:if_splits option.splits)

done

lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>

  \<Longrightarrow> flag = flag'"

apply (induct s arbitrary:p flag flag')

apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

done

lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"

apply (induct s arbitrary:p flag)

apply (simp, drule init_procs_has_shm, simp)

apply (frule vd_cons, frule vt_grant_os)

apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

done

lemma procs_of_shm_prop4':

  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"

by (auto dest:procs_of_shm_prop4)

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

end

end