--- a/Current_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Current_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -67,15 +67,18 @@
 
 lemma has_same_inode_in_current:
   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
-by (auto simp add:has_same_inode_def current_files_def)
+by (auto simp add:has_same_inode_def current_files_def same_inode_files_def 
+  is_file_def split:if_splits option.splits)
+
 
 lemma has_same_inode_prop1:
   "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
-by (auto simp:has_same_inode_def is_file_def)
+by (auto simp:has_same_inode_def same_inode_files_def is_file_def)
 
 lemma has_same_inode_prop1':
   "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
-by (auto simp:has_same_inode_def is_file_def)
+by (auto simp:has_same_inode_def is_file_def same_inode_files_def 
+ split:if_splits option.splits)
 
 lemma has_same_inode_prop2:
   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"