--- a/Init_prop.thy	Fri May 10 10:23:34 2013 +0800
+++ b/Init_prop.thy	Wed May 15 11:21:39 2013 +0800
@@ -273,7 +273,7 @@
 
 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)
+by (simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
 
 lemma init_same_inode_prop1:
   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
@@ -282,6 +282,19 @@
 apply (auto simp:init_files_prop1)
 done
 
+lemma init_same_inode_prop2:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f \<in> init_files\<rbrakk> \<Longrightarrow> f' \<in> init_files"
+by (drule init_same_inode_prop1, simp)
+
+lemma init_same_inode_prop3:
+  "f' \<in> init_same_inode_files f \<Longrightarrow> f \<in> init_same_inode_files f'"
+by (auto simp add:init_same_inode_files_def is_init_file_def split:if_splits)
+
+lemma init_same_inode_prop4:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f' \<in> init_files\<rbrakk> \<Longrightarrow> f \<in> init_files"
+apply (drule init_same_inode_prop3)
+by (simp add:init_same_inode_prop2)
+
 end
 
 context flask begin
@@ -558,7 +571,7 @@
 by (simp add:init_cf2sfile_def)
 
 lemma sroot_valid':
-  "cf2sfile s [] False = Some sroot"
+  "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)  
 
 lemma init_sectxt_prop:
@@ -646,51 +659,42 @@
 apply (simp add:init_cq2smsgq_def)
 by (case_tac sec, simp+)
 
-lemma cf2sfile_nil_prop1:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f (is_init_file f) = init_cf2sfile f"
+lemma cf2sfile_nil_prop:
+  "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 apply (case_tac f)
 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
-apply (rule notI, drule root_is_init_dir', simp)
 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
-apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
+apply (auto simp:is_init_file_def is_init_dir_def is_file_nil split:option.splits t_inode_tag.splits 
             dest:init_file_has_inum inof_has_file_tag)
 done
 
-
 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"
 apply (drule init_sectxt_prop2)+
 apply (auto intro:init_file_dir_conflict)
 done
 
-lemma cf2sfile_nil_prop2:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f (\<not> is_init_file f) = None"
-apply (case_tac f)
-apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
-apply (rule notI, drule root_is_init_dir', simp)
-apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
-apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
-            dest:init_file_has_inum inof_has_file_tag init_sec_file_dir)
-done
-
-lemma cf2sfile_nil_prop:
-  "f \<in> init_files \<Longrightarrow> cf2sfile [] f = (\<lambda> b. if (b = is_init_file f) then init_cf2sfile f else None)"
-apply (frule cf2sfile_nil_prop1, frule cf2sfile_nil_prop2)
-by (rule ext, auto split:if_splits)
-
 lemma cf2sfile_nil_prop3:
-  "is_init_file f \<Longrightarrow> cf2sfile [] f True = init_cf2sfile f"
+  "is_init_file f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
 
 lemma cf2sfile_nil_prop4:
-  "is_init_dir f \<Longrightarrow> cf2sfile [] f False = init_cf2sfile f"
+  "is_init_dir f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 apply (frule init_file_dir_conflict2)
 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
 
 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)
-apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits)
+  "f \<in> init_files \<Longrightarrow> cf2sfiles [] f = init_cf2sfiles f"
+apply (simp add:cf2sfiles_def init_cf2sfiles_def)
+apply (rule set_eqI, rule iffI, auto split:if_splits)
+apply (rule_tac x = f' in bexI, simp add:same_inode_nil_prop cf2sfile_nil_prop)
+apply (drule init_same_inode_prop2, simp)
+apply (simp add:cf2sfile_nil_prop)
+apply (simp add:same_inode_nil_prop)
+apply (rule_tac x = f' in bexI)
+apply (drule init_same_inode_prop2, simp)
+apply ( simp add:same_inode_nil_prop cf2sfile_nil_prop)
+apply (simp add:same_inode_nil_prop)
 done
 
 lemma cfd2sfd_nil_prop:
@@ -762,7 +766,7 @@
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 apply (simp add:init_files_props)
-apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict)
+apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict)
 done
 
 lemma s2ss_nil_prop: