# HG changeset patch # User chunhan # Date 1368752687 -28800 # Node ID 87fdf2de0ffaa0a284631e21fbcbc993d784c94b # Parent 289a30c4cfb7ef9deef6948696ee6520e3845c0b update proof scripts after Rmdir case 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: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> 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: + "\<lbrakk>f \<in> files_hung_by_del s; inum_of_file s f = Some im; valid s\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> 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 \<Longrightarrow> ( + (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> inum_of_file s f \<noteq> None) \<and> + (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> 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: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> inum_of_file s f \<noteq> None" + and isf: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> is_file s f" + by (auto dest:vd_cons vt_grant_os) + from pfd have pfd': "\<And> p fd f. inum_of_file s f = None \<Longrightarrow> file_of_proc_fd s p fd \<noteq> Some f" + by (rule_tac notI, drule_tac pfd, simp) + + have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> inum_of_file (e # s) f \<noteq> 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 "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> 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: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" -apply (induct \<tau>) -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': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> 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: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> 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: - "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE" -apply (induct \<tau> 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: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> 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': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> 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: + "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> 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: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" @@ -489,7 +530,7 @@ lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)" by (auto simp:current_files_def inum_of_file.simps split:option.splits) -lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then current_files \<tau> - {f} else current_files \<tau>)" +lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = current_files \<tau> - {f}" by (auto simp:current_files_def inum_of_file.simps split:option.splits) lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)" @@ -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: