44 |
45 |
45 lemma not_init_intro_proc': |
46 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 "\<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 using not_deleted_init_proc by auto |
48 |
49 |
|
50 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" |
|
52 by (auto simp add:has_same_inode_def current_files_def) |
|
53 |
|
54 lemma has_same_inode_prop1: |
|
55 "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
|
56 by (auto simp:has_same_inode_def is_file_def) |
|
57 |
|
58 lemma has_same_inode_prop1': |
|
59 "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f" |
|
60 by (auto simp:has_same_inode_def is_file_def) |
|
61 |
|
62 lemma has_same_inode_prop2: |
|
63 "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
|
64 apply (drule has_same_inode_prop1) |
|
65 apply (simp add:file_of_pfd_is_file, simp+) |
|
66 done |
|
67 |
|
68 lemma has_same_inode_prop2': |
|
69 "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f" |
|
70 apply (drule has_same_inode_prop1') |
|
71 apply (simp add:file_of_pfd_is_file, simp+) |
|
72 done |
|
73 |
|
74 lemma tobj_in_init_alive: |
|
75 "tobj_in_init obj \<Longrightarrow> init_alive obj" |
|
76 by (case_tac obj, auto) |
|
77 |
|
78 lemma tobj_in_alive: |
|
79 "tobj_in_init obj \<Longrightarrow> alive [] obj" |
|
80 by (case_tac obj, auto simp:is_file_nil) |
|
81 |
49 end |
82 end |
50 |
83 |
51 end |
84 end |