--- a/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 14:39:00 2014 +0800
+++ b/no_shm_selinux/New_obj_prop.thy	Thu Jan 09 19:09:09 2014 +0800
@@ -63,31 +63,57 @@
 lemma len_fname_all: "length (fname_all_a len) = len"
 by (induct len, auto simp:fname_all_a.simps)
 
-lemma ncf_notin_curf: "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> current_files \<tau>"
-apply (drule finite_cf)
-apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)
-apply (rule notI)
-apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> {fn. fn # f \<in> current_files \<tau>}")
-defer apply simp
-apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> fname_length_set {fn. fn # f \<in> current_files \<tau>}")
-defer apply (auto simp:fname_length_set_def image_def)[1]
-apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files \<tau>})")  
-defer
-apply (simp add:fname_length_set_def) 
-apply (rule finite_imageI)
+lemma finite_fs_fnames:
+  "finite (fs::t_file set) \<Longrightarrow> finite {fn. fn # f \<in> fs}"
+thm finite_imageI
 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
-apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files \<tau>)" in finite_subset)
+apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` fs)" in finite_subset)
 unfolding image_def
 apply (clarsimp  split:if_splits)
-apply (rule_tac x = "x # f" in bexI, simp+)
+apply (rule_tac x = "x # f" in bexI, simp+) 
+done
 
-apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files \<tau>})" in nn_notin_aux)
-apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>})))" in ballE)
-apply (simp add:len_fname_all, simp)
+lemma ncf_notin_curf_aux:
+  "finite (fs::t_file set) \<Longrightarrow> Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> fname_length_set {fn. fn # f \<in> fs}"
+apply (drule_tac f = f in finite_fs_fnames)
+apply (drule_tac h = length in finite_imageI)
+apply (simp add:fname_length_set_def)
+apply (drule nn_notin_aux)
+apply auto
 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)"
+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)}"
+    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}"
+    by (auto simp:fname_length_set_def)
+  show ?thesis
+    apply (simp only:new_childf_general_def next_fname_def all_fname_under_dir_def)
+    apply (rule notI)
+    apply (drule a2, drule a3)
+    apply (simp only:len_fname_all)
+    using a1 by auto
+qed
+  
+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 (simp add:new_childf_def)
+done
+
+lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f \<tau> fs) = Some f"
+by (simp add:new_childf_general_def)
+
 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"
-by (simp add:new_childf_def)
+by (simp add:new_childf_def ncf_parent_general)
 
 end