# HG changeset patch
# User chunhan
# Date 1367978438 -28800
# Node ID b6ee5f35c41f2da94550de529b72fc08dbb2b5ae
# Parent  5a01ee1c9b4de98ec6542c5f437479ad27a5a6f1
update

diff -r 5a01ee1c9b4d -r b6ee5f35c41f Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Mon May 06 02:04:27 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 08 10:00:38 2013 +0800
@@ -18,11 +18,18 @@
           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
 
+lemma sroot_only:
+  "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)"
+by (rule ext, simp add:cf2sfile_def)
+
 lemma cf2sfile_open_some1:
   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>
    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)
-apply (induct f')
+apply (induct f', simp add:sroot_only)
+apply simp
+apply (frule parentf_in_current', simp+)
+apply (auto simp:cf2sfile_def split:if_splits option.splits)
 apply (auto  split:if_splits option.splits    dest!:current_has_sec'
           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)