diff -r 9b42765ce554 -r ced0fcfbcf8e Tainted_prop.thy
--- a/Tainted_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Tainted_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1,20 +1,46 @@
 theory Tainted_prop 
-imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop
 begin
 
 context tainting begin
 
 lemma tainted_in_current:
-  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
-apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)
+  "obj \<in> tainted s \<Longrightarrow> alive s obj"
+apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)
+apply (drule seeds_in_init, simp add:tobj_in_alive)
+apply (erule has_same_inode_prop2, simp, simp add:vd_cons)
+apply (frule vt_grant_os, simp)
+apply (erule has_same_inode_prop1, simp, simp add:vd_cons)
+done
+
+lemma tainted_is_valid:
+  "obj \<in> tainted s \<Longrightarrow> valid s"
+by (erule tainted.induct, auto intro:valid.intros)
 
+lemma t_remain_app:
+  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> 
+  \<Longrightarrow> obj \<in> tainted (s' @ s)"
+apply (induct s', simp)
+apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)
+apply (simp_all add:not_deleted_cons_D vd_cons)
+apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)
+done
 
+lemma valid_tainted_obj:
+  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)"
+apply (erule tainted.induct)
+apply (drule seeds_in_init)
+by auto
 
+lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
+
+lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
+
+lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
 
 end
 
-end
-
-
-
-
+end
\ No newline at end of file