--- a/Co2sobj_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -8,8 +8,6 @@
 
 (************ simpset for cf2sfile ***************)
 
-declare get_parentfs_ctxts.simps [simp del]
-
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)
@@ -71,6 +69,49 @@
 apply (auto simp:cf2sfile_def split:if_splits option.splits)
 done
 
+lemma sroot_set:
+  "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"
+apply (frule root_is_dir)
+apply (drule is_dir_has_sec, simp)
+apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 
+                 root_type_remains root_user_remains
+           dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'
+           split:option.splits)
+done
+
+lemma cf2sfile_path_file:
+  "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>
+   \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
+          (case (sectxt_of_obj s (O_file (f # pf))) of
+              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+           | None \<Rightarrow> None)
+     | _ \<Rightarrow> None)"
+apply (frule is_file_in_current, drule parentf_is_dir'', simp)
+apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
+apply (frule sroot_set)
+apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
+done
+
+lemma cf2sfile_path_dir:
+  "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>
+   \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
+          (case (sectxt_of_obj s (O_dir (f # pf))) of
+              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
+                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+           | None \<Rightarrow> None)
+     | _ \<Rightarrow> None)"
+apply (frule is_dir_in_current, drule parentf_is_dir'', simp)
+apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)
+apply (frule_tac f = "pf" in is_dir_has_sfile, simp)
+apply (frule sroot_set)
+apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
+done  
+
 lemma cf2sfile_path:
   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
      case (cf2sfile s pf) of
@@ -80,16 +121,38 @@
                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
                | None \<Rightarrow> None)
          else (case (sectxt_of_obj s (O_dir (f # pf))) of
-                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
                | None \<Rightarrow> None)           )
      | None \<Rightarrow> None)"
+apply (drule is_file_or_dir, simp)
+apply (erule disjE)
+apply (frule cf2sfile_path_file, simp) defer
+apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)
+apply (auto split:option.splits)
+done
+
+
+
+apply simp
+
+thm cf2sfile_def
+apply (simp (no_asm_simp))
+apply simp
+apply (frule cf2sfile_path_file, simp)
+apply (simp add: cf2sfile_path_file)
+apply auto
+apply (simp only:cf2sfile_path_file)
+by (simp add:cf2sfile_path_file cf2sfile_path_dir)
 apply (frule parentf_is_dir'', simp)
-apply (frule parentf_in_current', simp)
 apply (frule is_file_or_dir, simp)
-apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE)
-apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop
-            simp:cf2sfile_def split:option.splits if_splits)
+apply (frule sroot_set, erule disjE)
+apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
+apply (case_tac pf, clarsimp)
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps
+            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop 
+            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
 apply (case_tac "is_file s (f # pf)")
 apply (frule is_file_has_sec, simp)
 apply (frule is_dir_has_sec, simp)