1 theory Current_prop

     2 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop

     3 begin

     4 (*<*)

     5 

     6 context flask begin

     7 

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

     9 apply (induct s arbitrary:p_flag)

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

    11 apply (frule vd_cons, frule vt_grant_os)

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

    13 done

    14 

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

    16 apply (induct s arbitrary:p flag)

    17 apply (simp, drule init_procs_has_shm, simp)

    18 apply (frule vd_cons, frule vt_grant_os)

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

    20 done

    21 

    22 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>

    23   \<Longrightarrow> flag = flag'"

    24 apply (induct s arbitrary:p flag flag')

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

    26 apply (frule vd_cons, frule vt_grant_os)

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

    28 done

    29 

    30 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"

    31 apply (induct s arbitrary:p flag)

    32 apply (simp, drule init_procs_has_shm, simp)

    33 apply (frule vd_cons, frule vt_grant_os)

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

    35 done

    36 

    37 lemma procs_of_shm_prop4':

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

    39 by (auto dest:procs_of_shm_prop4)

    40 

    41 lemma not_init_intro_proc:

    42   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"

    43 using not_deleted_init_proc by auto

    44 

    45 lemma not_init_intro_proc':

    46   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"

    47 using not_deleted_init_proc by auto

    48 

    49 end

    50 

    51 end