--- a/Co2sobj_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -10,13 +10,28 @@
 
 declare get_parentfs_ctxts.simps [simp del]
 
-lemma cf2sfile_open_none:
+lemma cf2sfile_open_none1:
   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b"
 apply (frule vd_cons, frule vt_grant_os)
-apply (frule noroot_events)
-by (auto split:if_splits option.splits    dest!:current_has_sec'
+apply (frule noroot_events, case_tac f, simp)
+apply (auto split:if_splits option.splits    dest!:current_has_sec' dest:parentf_in_current'
           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
+done
+
+lemma cf2sfile_open_none2:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b"
+apply (frule vd_cons, frule vt_grant_os)
+apply (induct f', simp add:cf2sfile_def)
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps)
+done
+
+lemma cf2sfile_open_none:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"
+apply (rule ext, rule ext)
+apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2)
+done
 
 lemma sroot_only:
   "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)"
@@ -26,12 +41,10 @@
   "\<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', simp add:sroot_only)
-apply simp
+apply (case_tac "f = f'", simp)
+apply (induct f', simp add:sroot_only, 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 
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
 done
 
@@ -56,6 +69,11 @@
                   | _ \<Rightarrow> None)
      | None \<Rightarrow> None)"
 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac f, simp)
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps)
+apply (rule impI)
+thm not_deleted_imp_exists
 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)