--- a/Current_files_prop.thy Wed Sep 04 09:07:39 2013 +0800
+++ b/Current_files_prop.thy Wed Sep 04 09:58:30 2013 +0800
@@ -768,6 +768,139 @@
lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir'
noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate'
+
+lemma is_file_in_current:
+ "is_file s f \<Longrightarrow> f \<in> current_files s"
+by (auto simp:is_file_def current_files_def split:option.splits)
+
+lemma is_dir_in_current:
+ "is_dir s f \<Longrightarrow> f \<in> current_files s"
+by (auto simp:is_dir_def current_files_def split:option.splits)
+
+
+(* simpset for same_inode_files: Current_files_prop.thy *)
+
+lemma same_inode_files_nil:
+ "same_inode_files [] = init_same_inode_files"
+by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
+
+lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+by (auto simp add:current_inode_nums_def current_file_inums_def)
+
+lemma same_inode_files_open:
+ "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.
+ if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim')
+apply (drule is_file_in_current)
+apply (simp add:current_files_def)
+done
+
+lemma same_inode_files_linkhard:
+ "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'.
+ if (f' = f \<or> f' \<in> same_inode_files s oldf)
+ then same_inode_files s oldf \<union> {f}
+ else same_inode_files s f')"
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim')
+apply (drule is_file_in_current)
+apply (simp add:current_files_def is_file_def)
+apply (simp add:is_file_def)
+done
+
+lemma inum_of_file_none_prop:
+ "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (simp add:current_files_def)
+
+lemma same_inode_files_closefd:
+ "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow>
+ same_inode_files (CloseFd p fd # s) f' = (
+ case (file_of_proc_fd s p fd) of
+ Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
+ then same_inode_files s f' - {f}
+ else same_inode_files s f' )
+ | None \<Rightarrow> same_inode_files s f' )"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd
+ split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
+done
+
+lemma same_inode_files_unlink:
+ "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
+ \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (
+ if (proc_fd_of_file s f = {})
+ then same_inode_files s f' - {f}
+ else same_inode_files s f')"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink
+ split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
+done
+
+lemma same_inode_files_mkdir:
+ "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:same_inode_files_def is_file_simps current_files_simps
+ split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)
+apply (simp add:current_files_def is_file_def)
+done
+
+lemma same_inode_files_other:
+ "\<lbrakk>valid (e # s);
+ \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p f. e \<noteq> UnLink p f;
+ \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s) = same_inode_files s"
+apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)
+apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def
+ split:if_splits option.splits
+ dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)
+apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+
+done
+
+lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard
+ same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other
+
+lemma same_inode_files_prop1:
+ "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"
+by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)
+
+lemma same_inode_files_prop2:
+ "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"
+by (auto dest:same_inode_files_prop1)
+
+lemma same_inode_files_prop3:
+ "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
+apply (rule notI)
+apply (simp add:same_inode_files_def is_file_def is_dir_def
+ split:if_splits option.splits t_inode_tag.splits)
+done
+
+lemma same_inode_files_prop4:
+ "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
+by (auto simp:same_inode_files_def split:if_splits)
+
+lemma same_inode_files_prop5:
+ "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
+lemma same_inode_files_prop6:
+ "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
+lemma same_inode_files_prop7:
+ "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+
+lemma same_inode_files_prop8:
+ "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+
+
end
end
\ No newline at end of file