--- a/Finite_current.thy	Wed Nov 20 16:24:16 2013 +0800
+++ b/Finite_current.thy	Wed Nov 20 18:51:51 2013 +0800
@@ -1,5 +1,5 @@
 theory Finite_current
-imports Main Valid_prop Flask Flask_type
+imports Main Valid_prop Flask Flask_type Proc_fd_of_file_prop
 begin
 
 context flask begin
@@ -31,8 +31,13 @@
 apply (induct \<tau> arbitrary:p)
 apply (simp add:current_proc_fds.simps init_finite_sets)
 apply (frule vd_cons, frule vt_grant_os, case_tac a, auto simp:current_proc_fds.simps)
-apply (metis double_diff equalityE finite_Diff)
-by (metis double_diff finite_Diff subset_refl)
+apply (erule finite_subset)
+apply (frule_tac s = \<tau> and p = nat in file_fds_subset_pfds)
+apply (erule finite_subset, simp)
+apply (erule finite_subset)
+apply (frule_tac s = \<tau> and p = nat1 in file_fds_subset_pfds)
+apply (erule finite_subset, simp)
+done
 
 lemma finite_pair: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> A \<and> y \<in> B}"
 by auto