--- a/Sectxt_prop.thy	Wed May 15 15:42:46 2013 +0800
+++ b/Sectxt_prop.thy	Thu May 16 15:18:44 2013 +0800
@@ -617,11 +617,16 @@
 apply (rule_tac f = "x # pf" in parentf_is_dir)
 by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits)
 
-lemma get_pfs_secs_prop:
+lemma get_pfs_secs_prop':
   "\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
 apply (induct f)
 by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1)
 
+lemma get_pfs_secs_prop:
+  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> asecs. get_parentfs_ctxts s f = Some asecs"
+using get_pfs_secs_prop'
+by (auto)
+
 lemma get_pfs_secs_open:
   "valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s"
 apply (frule noroot_events, frule vd_cons, frule vt_grant_os)
@@ -656,7 +661,7 @@
     from p1 os have p5: "f' \<noteq> f"  by (auto simp:is_dir_in_current)
     show ?case using mkdir vd os p4 p5  p1
       by (auto simp:sectxt_of_obj_simps is_dir_simps p3
-              split:option.splits   dest:current_has_sec' get_pfs_secs_prop)
+              split:option.splits   dest:current_has_sec' get_pfs_secs_prop')
   qed
 qed
 
@@ -669,7 +674,7 @@
                | _ \<Rightarrow> None))"
 apply (frule vd_cons, frule vt_grant_os)
 apply (frule noroot_events, case_tac f)
-by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop get_pfs_secs_mkdir1
+by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop' get_pfs_secs_mkdir1
           simp:sectxt_of_obj_simps is_dir_simps)
 
 lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2