--- a/Flask.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Flask.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -311,38 +311,6 @@
 where
   "current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}" 
 
-definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
-where 
-  "has_same_inode \<tau> fa fb = 
-     (\<exists>i. inum_of_file \<tau> fa = Some i \<and> inum_of_file \<tau> fb = Some i)"
-
-fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
-where
-  "inum_of_socket [] = init_inum_of_socket"
-| "inum_of_socket (CloseFd p fd # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd):= None)"
-| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd) := Some ino)"
-| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd') := Some ino)"
-| "inum_of_socket (Clone p p' fds shms # \<tau>) = 
-     (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) 
-                   else if (p'' = p') then None
-                   else inum_of_socket \<tau> (p'',fd))" 
-| "inum_of_socket (Execve p f fds # \<tau>) = 
-     (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
-                  else if (p' = p) then None
-                  else inum_of_socket \<tau> (p', fd))"
-| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 
-     (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"
-| "inum_of_socket (Exit p # \<tau>) = 
-     (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"
-| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>" 
-
-definition current_sockets :: "t_state \<Rightarrow> t_socket set"
-where
-  "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
-
 (* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)  
 (* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)
 fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"
@@ -378,6 +346,41 @@
 where
   "dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"
 
+definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
+where
+  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
+
+definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
+where 
+  "has_same_inode s fa fb \<equiv> fb \<in> same_inode_files s fa"
+
+fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
+where
+  "inum_of_socket [] = init_inum_of_socket"
+| "inum_of_socket (CloseFd p fd # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd):= None)"
+| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd) := Some ino)"
+| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd') := Some ino)"
+| "inum_of_socket (Clone p p' fds shms # \<tau>) = 
+     (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) 
+                   else if (p'' = p') then None
+                   else inum_of_socket \<tau> (p'',fd))" 
+| "inum_of_socket (Execve p f fds # \<tau>) = 
+     (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
+                  else if (p' = p) then None
+                  else inum_of_socket \<tau> (p', fd))"
+| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 
+     (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"
+| "inum_of_socket (Exit p # \<tau>) = 
+     (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"
+| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>" 
+
+definition current_sockets :: "t_state \<Rightarrow> t_socket set"
+where
+  "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
+
 definition is_tcp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
 where
   "is_tcp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of
@@ -522,10 +525,6 @@
 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> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
-
 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"