--- 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: