--- a/Current_files_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Current_files_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -215,25 +215,27 @@
 
       have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"
         apply (clarify, case_tac a) using os fin
-        apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def 
+        apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def 
                    split:if_splits option.splits)
         done
       moreover 
       have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" 
         apply (clarify, case_tac a)
         using vt os pin'
-        apply (auto simp:os_grant.simps current_files_def inum_of_file.simps split:if_splits option.splits)
+        apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def 
+                   split:if_splits option.splits t_inode_tag.splits)
         apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)
-        apply (drule_tac f = list and f' = f in fns', simp, simp, simp)
-        apply (drule_tac f = list and f' = f in dns', simp, simp, simp)
+        apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp)
+        apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp)
         done
       moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"
         apply (clarify, case_tac a)    
-        using vt os fns''
+        using vt os fns'' cons
         apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps 
                          is_file_def is_dir_def 
                     dest:ios's_im_in_cim iof's_im_in_cim
-                   split:if_splits option.splits t_inode_tag.splits t_socket_type.splits)
+                   split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) 
+        apply (rule_tac im = a and f = f and f' = f' in fns'', simp+)
         apply (drule_tac f = f' and pf = list in pin', simp, simp)
         apply (drule_tac f = f' and pf = list2 in pin', simp, simp)
         done
@@ -370,7 +372,7 @@
 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 
+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)+  
@@ -496,7 +498,7 @@
 lemma current_files_linkhard: 
   "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"
 apply (frule vt_grant_os, frule vd_cons)
-by (auto simp:current_files_def inum_of_file.simps os_grant.simps split:option.splits)
+by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits)
 
 (*
 lemma rename_renaming_decom: