--- a/Current_files_prop.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Current_files_prop.thy	Mon May 06 02:04:27 2013 +0800
@@ -539,9 +539,6 @@
 
 (******************** is_file simpset *********************)
 
-lemma is_file_nil: "is_file [] = is_init_file"
-by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
-
 lemma is_file_open:
   "valid (Open p f flags fd opt # s) \<Longrightarrow> 
    is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))"
@@ -606,9 +603,6 @@
 
 (********* is_dir simpset **********)
 
-lemma is_dir_nil: "is_dir [] = is_init_dir"
-by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
-
 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)"
 apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext

--- 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" 

--- a/Init_prop.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Init_prop.thy	Mon May 06 02:04:27 2013 +0800
@@ -84,6 +84,12 @@
 
 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2
 
+lemma is_file_nil: "is_file [] = is_init_file"
+by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
+
+lemma is_dir_nil: "is_dir [] = is_init_dir"
+by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
+
 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
@@ -236,6 +242,16 @@
 apply (erule_tac x = f' in allE, simp)
 by (case_tac f', simp_all add:no_junior_def)
 
+lemma same_inode_nil_prop:
+  "same_inode_files [] f = init_same_inode_files f"
+by (simp add:same_inode_files_def init_same_inode_files_def)
+
+lemma init_same_inode_prop1:
+  "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
+apply (simp add:init_same_inode_files_def)
+apply (drule init_files_prop3)
+apply (auto simp:init_files_prop1)
+done
 
 end
 
@@ -350,8 +366,27 @@
 
 lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5
 
+lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
 end
 
+context tainting begin
+
+lemma tainted_nil_prop:
+  "(x \<in> tainted []) = (x \<in> seeds)"
+apply (rule iffI)
+apply (erule tainted.cases, simp+)
+apply (erule t_init)
+done
+
+end
 
 context tainting_s begin
 
@@ -592,14 +627,6 @@
             dest:init_file_has_inum inof_has_file_tag)
 done
 
-lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
-by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
-
-lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
-by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
-
-lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
-by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
 
 lemma init_sec_file_dir:
   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
@@ -634,12 +661,13 @@
 lemma cfs2sfiles_nil_prop:
   "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs"
 apply (simp add:cfs2sfiles_def init_cfs2sfiles_def)
-using cf2sfile_nil_prop apply auto
+apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits)
+done
 
 lemma cfd2sfd_nil_prop:
   "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"
 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)
-apply (drule init_filefd_prop1, drule cf2sfile_nil_prop)
+apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop)
 by (auto split:option.splits)
 
 lemma cpfd2sfds_nil_prop:
@@ -668,13 +696,6 @@
 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cph2spshs_nil_prop cpfd2sfds_nil_prop
          split:option.splits)
 
-lemma tainted_nil_prop:
-  "(x \<in> tainted []) = (x \<in> seeds)"
-apply (rule iffI)
-apply (erule tainted.cases, simp+)
-apply (erule t_init)
-done
-
 lemma msg_has_sec_imp_init: 
   "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
 apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -701,27 +722,19 @@
 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
             intro:msgq_has_sec_imp_init split:option.splits)
 
-lemma same_inode_nil_prop:
-  "same_inode_files [] f = init_same_inode_files f"
-by (simp add:same_inode_files_def init_same_inode_files_def)
-
-lemma init_same_inode_prop1:
-  "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
-apply (simp add:init_same_inode_files_def)
-apply (drule init_files_prop3)
-apply (auto simp:init_files_prop1)
-done
-
 lemma co2sobj_nil_prop:
   "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
 apply (case_tac obj)
 apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 
                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop 
-                     same_inode_nil_prop  cm2smsg_nil_prop dest:init_same_inode_prop1 
+                     same_inode_nil_prop  cm2smsg_nil_prop 
+            dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
-by (simp add:init_files_props)
+apply (simp add:init_files_props)
+apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict)
+done
 
 lemma s2ss_nil_prop:
   "s2ss [] = init_static_state"

--- a/Static.thy	Fri May 03 08:20:21 2013 +0100
+++ b/Static.thy	Mon May 06 02:04:27 2013 +0800
@@ -51,7 +51,7 @@
 
 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set"
 where
-  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf}"
+  "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}"
 
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
@@ -109,10 +109,6 @@
        (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
      | _ \<Rightarrow> None)"
 
-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_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
 where
   "init_obj2sobj (O_proc p) = 
@@ -720,10 +716,6 @@
 where
   "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}"
 
-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'}"
-
 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
 where