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