65 |
65 |
66 |
66 |
67 |
67 |
68 lemma has_same_inode_in_current: |
68 lemma has_same_inode_in_current: |
69 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
69 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
70 by (auto simp add:has_same_inode_def current_files_def) |
70 by (auto simp add:has_same_inode_def current_files_def same_inode_files_def |
|
71 is_file_def split:if_splits option.splits) |
|
72 |
71 |
73 |
72 lemma has_same_inode_prop1: |
74 lemma has_same_inode_prop1: |
73 "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
75 "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
74 by (auto simp:has_same_inode_def is_file_def) |
76 by (auto simp:has_same_inode_def same_inode_files_def is_file_def) |
75 |
77 |
76 lemma has_same_inode_prop1': |
78 lemma has_same_inode_prop1': |
77 "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f" |
79 "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f" |
78 by (auto simp:has_same_inode_def is_file_def) |
80 by (auto simp:has_same_inode_def is_file_def same_inode_files_def |
|
81 split:if_splits option.splits) |
79 |
82 |
80 lemma has_same_inode_prop2: |
83 lemma has_same_inode_prop2: |
81 "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
84 "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'" |
82 apply (drule has_same_inode_prop1) |
85 apply (drule has_same_inode_prop1) |
83 apply (simp add:file_of_pfd_is_file, simp+) |
86 apply (simp add:file_of_pfd_is_file, simp+) |