--- a/Flask.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Flask.thy	Mon May 06 02:04:27 2013 +0800
@@ -204,6 +204,10 @@
                                       | _                 \<Rightarrow> False)
                          | _      \<Rightarrow> False)"
 
+definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
+where
+  "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
+
 fun init_alive :: "t_object \<Rightarrow> bool"
 where
   "init_alive (O_proc p)     = (p \<in> init_procs)"
@@ -475,6 +479,10 @@
 where
   "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>"
 
+definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
+where
+  "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}"
+
 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
 where
   "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd"