770 lemma cf2sfile_closefd: |
770 lemma cf2sfile_closefd: |
771 "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk> |
771 "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk> |
772 \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f" |
772 \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f" |
773 apply (frule vd_cons, frule vt_grant_os) |
773 apply (frule vd_cons, frule vt_grant_os) |
774 apply (simp add:current_files_simps split:if_splits option.splits) |
774 apply (simp add:current_files_simps split:if_splits option.splits) |
775 (* costs too much time, but solved |
775 (* costs too much time, but solved *) |
776 |
776 |
777 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps |
777 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps |
778 split:if_splits option.splits |
778 split:if_splits option.splits |
779 dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file |
779 dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file |
780 not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file |
780 not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file |
781 dest!:current_has_sec') |
781 dest!:current_has_sec') |
782 done |
782 done |
783 *) |
|
784 sorry |
|
785 |
783 |
786 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other |
784 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other |
787 cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd |
785 cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd |
788 |
786 |
789 (*********** cfd2sfd simpset *********) |
787 (*********** cfd2sfd simpset *********) |