equal
deleted
inserted
replaced
45 |
45 |
46 lemma not_init_intro_proc': |
46 lemma not_init_intro_proc': |
47 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
47 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
48 using not_deleted_init_proc by auto |
48 using not_deleted_init_proc by auto |
49 |
49 |
|
50 lemma info_shm_flow_in_procs: |
|
51 "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s" |
|
52 by (auto simp:info_flow_shm_def intro:procs_of_shm_prop2) |
|
53 |
50 lemma has_same_inode_in_current: |
54 lemma has_same_inode_in_current: |
51 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
55 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
52 by (auto simp add:has_same_inode_def current_files_def) |
56 by (auto simp add:has_same_inode_def current_files_def) |
53 |
57 |
54 lemma has_same_inode_prop1: |
58 lemma has_same_inode_prop1: |