--- a/Current_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Current_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1,7 +1,8 @@
+(*<*)
 theory Current_prop
 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
 begin
-(*<*)
+(*>*)
 
 context flask begin
 
@@ -46,6 +47,38 @@
   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 using not_deleted_init_proc by auto
 
+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)
+
+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)
+
+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)
+
+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'"
+apply (drule has_same_inode_prop1)
+apply (simp add:file_of_pfd_is_file, simp+)
+done
+
+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"
+apply (drule has_same_inode_prop1')
+apply (simp add:file_of_pfd_is_file, simp+)
+done
+
+lemma tobj_in_init_alive:
+  "tobj_in_init obj \<Longrightarrow> init_alive obj"
+by (case_tac obj, auto)
+
+lemma tobj_in_alive:
+  "tobj_in_init obj \<Longrightarrow> alive [] obj"
+by (case_tac obj, auto simp:is_file_nil)
+
 end
 
 end
\ No newline at end of file