diff -r 289a30c4cfb7 -r 87fdf2de0ffa Current_files_prop.thy --- a/Current_files_prop.thy Thu May 16 15:18:44 2013 +0800 +++ b/Current_files_prop.thy Fri May 17 09:04:47 2013 +0800 @@ -359,27 +359,75 @@ lemma hung_file_no_des: "\f \ files_hung_by_del \; valid \; f' \ current_files \; f \ f'; f \ f'\ \ False" by (rule hung_file_no_des_aux[rule_format], blast) +(* current version, dir can not be opened, so hung_files are all files lemma hung_file_is_leaf: "\f \ files_hung_by_del \; valid \\ \ is_file \ f \ dir_is_empty \ f" apply (frule hung_file_has_inum', simp, erule exE) apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits) by (simp add: noJ_Anc, auto dest:hung_file_no_des) +*) +lemma hung_file_has_filetag: + "\f \ files_hung_by_del s; inum_of_file s f = Some im; valid s\ \ itag_of_inum s im = Some Tag_FILE" +apply (induct s) +apply (simp add:files_hung_by_del.simps) +apply (drule init_files_hung_prop2, (erule exE)+) +apply (drule init_filefd_prop5, clarsimp simp:is_init_file_def split:t_inode_tag.splits option.splits) + +apply (frule vd_cons, frule vt_grant_os, case_tac a) +apply (auto simp:files_hung_by_del.simps is_file_def is_dir_def current_files_def current_inode_nums_def + split:if_splits option.splits t_inode_tag.splits t_socket_type.splits + dest:hung_file_has_inum iof's_im_in_cim) +done + +lemma hung_file_is_file: "\f \ files_hung_by_del \; valid \\ \ is_file \ f" +apply (frule hung_file_has_inum', simp, erule exE) +apply (drule hung_file_has_filetag, auto simp:is_file_def) +done + +(*********************** 2 in 1 *********************) + +lemma file_of_pfd_2in1: "valid s \ ( + (\ p fd f. file_of_proc_fd s p fd = Some f \ inum_of_file s f \ None) \ + (\ p fd f. file_of_proc_fd s p fd = Some f \ is_file s f) )" +proof (induct s) + case Nil + show ?case + by (auto dest:init_filefd_valid simp:is_file_def) +next + case (Cons e s) + hence vd_e: "valid (e # s)" and vd_s: "valid s" and os: "os_grant s e" + and pfd: "\ p fd f. file_of_proc_fd s p fd = Some f \ inum_of_file s f \ None" + and isf: "\ p fd f. file_of_proc_fd s p fd = Some f \ is_file s f" + by (auto dest:vd_cons vt_grant_os) + from pfd have pfd': "\ p fd f. inum_of_file s f = None \ file_of_proc_fd s p fd \ Some f" + by (rule_tac notI, drule_tac pfd, simp) + + have "\p fd f. file_of_proc_fd (e # s) p fd = Some f \ inum_of_file (e # s) f \ None" + apply (case_tac e) using os + apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def + dir_is_empty_def is_file_def is_dir_def + split:if_splits option.splits dest:pfd) + apply (simp add:pfdof_simp3)+ + apply (simp add:proc_fd_of_file_def) + apply (drule isf, simp add:is_file_def split:t_inode_tag.splits) + done + moreover + have "\p fd f. file_of_proc_fd (e # s) p fd = Some f \ is_file (e # s) f" + apply (case_tac e) using os + apply (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits + dest:pfd isf iof's_im_in_cim + simp:is_file_def is_dir_def dir_is_empty_def current_files_def) + apply (simp add:pfdof_simp3)+ + apply (simp add:proc_fd_of_file_def) + done + ultimately show ?case by auto +qed (************** file_of_proc_fd in current ********************) -lemma file_of_pfd_imp_inode_aux: "\ p f. file_of_proc_fd \ p fd = Some f \ valid \ \ inum_of_file \ f \ None" -apply (induct \) -apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum) -apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a) -apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def is_file_def - split:if_splits option.splits) -apply (simp add:pfdof_simp3)+ -apply (simp add:proc_fd_of_file_def)+ -done - lemma file_of_pfd_imp_inode': "\file_of_proc_fd \ p fd = Some f; valid \\ \ inum_of_file \ f \ None" -by (rule file_of_pfd_imp_inode_aux[rule_format], blast) +by (drule file_of_pfd_2in1, blast) lemma file_of_pfd_imp_inode: "\file_of_proc_fd \ p fd = Some f; valid \\ \ \ im. inum_of_file \ f = Some im" by (auto dest!:file_of_pfd_imp_inode') @@ -390,25 +438,18 @@ (*************** file_of_proc_fd is file *********************) -lemma file_of_pfd_is_file_tag: - "\file_of_proc_fd \ p fd = Some f; valid \; inum_of_file \ f = Some im\ \ itag_of_inum \ im = Some Tag_FILE" -apply (induct \ arbitrary:p, simp) -apply (drule init_filefd_prop5, simp add:is_init_file_def split:option.splits t_inode_tag.splits) -apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) -by (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits - dest:file_of_pfd_imp_inode' iof's_im_in_cim - simp:is_file_def is_dir_def dir_is_empty_def current_files_def) - lemma file_of_pfd_is_file: "\file_of_proc_fd \ p fd = Some f; valid \\ \ is_file \ f" -apply (frule file_of_pfd_imp_inode, simp, erule exE) -apply (drule file_of_pfd_is_file_tag, simp+) -by (simp add:is_file_def) +by (drule file_of_pfd_2in1, auto simp:is_file_def) lemma file_of_pfd_is_file': "\file_of_proc_fd \ p fd = Some f; is_dir \ f; valid \\ \ False" by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) +lemma file_of_pfd_is_file_tag: + "\file_of_proc_fd \ p fd = Some f; valid \; inum_of_file \ f = Some im\ \ itag_of_inum \ im = Some Tag_FILE" +by (drule file_of_pfd_is_file, auto simp:is_file_def split:option.splits t_inode_tag.splits) + (************** parent file / ancestral file is dir *******************) lemma parentf_is_dir_aux: "\ f pf. parent f = Some pf \ inum_of_file \ f = Some im \ inum_of_file \ pf = Some ipm \ valid \ \ itag_of_inum \ ipm = Some Tag_DIR" @@ -489,7 +530,7 @@ lemma current_files_unlink: "current_files (UnLink p f # \) = (if (proc_fd_of_file \ f = {}) then (current_files \) - {f} else current_files \)" by (auto simp:current_files_def inum_of_file.simps split:option.splits) -lemma current_files_rmdir: "current_files (Rmdir p f # \) = (if (proc_fd_of_file \ f = {}) then current_files \ - {f} else current_files \)" +lemma current_files_rmdir: "current_files (Rmdir p f # \) = current_files \ - {f}" by (auto simp:current_files_def inum_of_file.simps split:option.splits) lemma current_files_mkdir: "current_files (Mkdir p f ino # \) = insert f (current_files \)" @@ -620,9 +661,6 @@ apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext split:if_splits option.splits t_inode_tag.split t_socket_type.splits simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) -apply (drule pfdof_simp2) -apply (drule file_of_pfd_is_file, simp) -apply (simp add:is_file_def split:t_inode_tag.splits option.splits) done lemma is_dir_other: