771 

   772 lemma is_file_in_current:

   773   "is_file s f \<Longrightarrow> f \<in> current_files s"

   774 by (auto simp:is_file_def current_files_def split:option.splits)

   775 

   776 lemma is_dir_in_current:

   777   "is_dir s f \<Longrightarrow> f \<in> current_files s"

   778 by (auto simp:is_dir_def current_files_def split:option.splits)

   779 

   780 

   781 (* simpset for same_inode_files: Current_files_prop.thy *)

   782 

   783 lemma same_inode_files_nil:

   784   "same_inode_files [] = init_same_inode_files"

   785 by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)

   786 

   787 lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"

   788 by (auto simp add:current_inode_nums_def current_file_inums_def)

   789 

   790 lemma same_inode_files_open:

   791   "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.

   792      if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"

   793 apply (frule vt_grant_os, frule vd_cons, rule ext)

   794 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

   795             dest:iof's_im_in_cim iof's_im_in_cim')

   796 apply (drule is_file_in_current)

   797 apply (simp add:current_files_def)

   798 done

   799 

   800 lemma same_inode_files_linkhard:

   801   "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. 

   802      if (f' = f \<or> f' \<in> same_inode_files s oldf) 

   803      then same_inode_files s oldf \<union> {f}

   804      else same_inode_files s f')"

   805 apply (frule vt_grant_os, frule vd_cons, rule ext)

   806 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

   807             dest:iof's_im_in_cim iof's_im_in_cim')

   808 apply (drule is_file_in_current)

   809 apply (simp add:current_files_def is_file_def)

   810 apply (simp add:is_file_def)

   811 done

   812 

   813 lemma inum_of_file_none_prop:

   814   "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   815 by (simp add:current_files_def)

   816 

   817 lemma same_inode_files_closefd:

   818   "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> 

   819    same_inode_files (CloseFd p fd # s) f' = (

   820      case (file_of_proc_fd s p fd) of 

   821        Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))

   822                  then same_inode_files s f' - {f}

   823                  else same_inode_files s f' )

   824      | None   \<Rightarrow> same_inode_files s f' )"

   825 apply (frule vt_grant_os, frule vd_cons)

   826 apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd 

   827            split:if_splits option.splits

   828             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

   829 done

   830 

   831 lemma same_inode_files_unlink:

   832   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> 

   833    \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (

   834      if (proc_fd_of_file s f = {}) 

   835      then same_inode_files s f' - {f}

   836      else same_inode_files s f')"

   837 apply (frule vt_grant_os, frule vd_cons)

   838 apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink 

   839            split:if_splits option.splits

   840             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

   841 done

   842 

   843 lemma same_inode_files_mkdir:

   844   "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"

   845 apply (frule vt_grant_os, frule vd_cons, rule ext)

   846 apply (auto simp:same_inode_files_def is_file_simps current_files_simps 

   847            split:if_splits option.splits

   848             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)

   849 apply (simp add:current_files_def is_file_def)

   850 done

   851 

   852 lemma same_inode_files_other:

   853   "\<lbrakk>valid (e # s); 

   854     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   855     \<forall> p fd. e \<noteq> CloseFd p fd;

   856     \<forall> p f. e \<noteq> UnLink p f;

   857     \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s)  = same_inode_files s"

   858 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)

   859 apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def

   860            split:if_splits option.splits

   861             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)

   862 apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+

   863 done

   864  

   865 lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard

   866   same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other

   867 

   868 lemma same_inode_files_prop1:

   869   "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"

   870 by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)

   871 

   872 lemma same_inode_files_prop2:

   873   "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   874 by (auto dest:same_inode_files_prop1)

   875 

   876 lemma same_inode_files_prop3:

   877   "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   878 apply (rule notI)

   879 apply (simp add:same_inode_files_def is_file_def is_dir_def 

   880           split:if_splits option.splits t_inode_tag.splits)

   881 done

   882 

   883 lemma same_inode_files_prop4:

   884   "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"

   885 by (auto simp:same_inode_files_def split:if_splits)

   886 

   887 lemma same_inode_files_prop5:

   888   "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"

   889 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   890 

   891 lemma same_inode_files_prop6:

   892   "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"

   893 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   894 

   895 lemma same_inode_files_prop7:

   896   "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"

   897 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   898 

   899 lemma same_inode_files_prop8:

   900   "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"

   901 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   902 

   903