--- a/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -83,13 +83,12 @@
 done
 
 lemma ncf_notin_curf_general:
-  assumes vd: "valid \<tau>" and fin_fs: "finite fs"
-  shows "new_childf_general f \<tau> fs \<notin> (current_files \<tau> \<union> fs)"
+  assumes fin_fs: "finite fs"
+  shows "new_childf_general f fs \<notin> fs"
 proof-
-  from vd fin_fs have "finite (current_files \<tau> \<union> fs)"
-    by (auto dest:finite_cf)
-  hence a1: "Suc (Max (fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)})) \<notin> 
-    fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)}"
+  have a1: "Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> 
+    fname_length_set {fn. fn # f \<in> fs}"
+    using fin_fs
     by (erule_tac ncf_notin_curf_aux)
   have a2: "\<And> f pf fs. f # pf \<in> fs \<Longrightarrow> f \<in> {fn. fn # pf \<in> fs}" by auto
   have a3: "\<And> f pf fs. f \<in> {fn. fn # pf \<in> fs} \<Longrightarrow> length f \<in> fname_length_set {fn. fn # pf \<in> fs}"
@@ -104,12 +103,12 @@
   
 lemma ncf_notin_curf:
  "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)"
-apply (drule_tac fs = "{}" in ncf_notin_curf_general)
-apply (simp)
+apply (drule finite_cf)
+apply (drule_tac fs = "current_files \<tau>" in ncf_notin_curf_general)
 apply (simp add:new_childf_def)
 done
 
-lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f \<tau> fs) = Some f"
+lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f fs) = Some f"
 by (simp add:new_childf_general_def)
 
 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"