--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tainted.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,53 @@
+theory tainted 
+imports Main rc_theory os_rc deleted_prop obj2sobj_prop
+begin
+
+context tainting begin
+
+lemma tainted_is_valid:
+  "obj \<in> tainted s \<Longrightarrow> valid s"
+by (erule tainted.induct, auto simp:vs_nil)
+
+lemma tainted_is_current:
+  "obj \<in> tainted s \<Longrightarrow> exists s obj"
+apply (erule tainted.induct)
+apply (auto dest:valid_os)
+apply (drule seeds_in_init, case_tac obj, auto)
+done
+
+lemma nodel_tainted_exists:
+  "\<lbrakk>no_del_event (s'@s); obj \<in> tainted s\<rbrakk> \<Longrightarrow> exists (s'@s) obj"
+apply (drule_tac obj = obj in nodel_imp_un_deleted)
+by (drule tainted_is_current, simp add:not_deleted_imp_exists')
+
+lemma t_remain_app:
+  "\<lbrakk>obj \<in> tainted s'; no_del_event (s @ s'); valid (s @ s')\<rbrakk> 
+  \<Longrightarrow> obj \<in> tainted (s @ s')"
+apply (induct s, simp)
+apply (simp only:cons_app_simp_aux)
+apply (frule valid_cons, frule no_del_event_cons_D, simp)
+apply (rule t_remain, simp+)
+apply (drule tainted_is_current)
+apply (case_tac a, case_tac [!] obj, auto)
+done
+
+end
+
+context tainting_s_complete begin
+
+lemma unknown_notin_tainted_s':
+  "sobj \<in> tainted_s \<Longrightarrow> sobj \<noteq> Unknown" 
+apply (erule tainted_s.induct, auto) 
+apply (drule seeds_in_init) 
+apply (subgoal_tac "exists [] obj")
+apply (drule init_obj_has_sobj, simp+)
+apply (case_tac obj, simp+)
+done
+
+lemma unknown_notin_tainted_s:
+  "Unknown \<in> tainted_s \<Longrightarrow> False"
+by (auto dest:unknown_notin_tainted_s')
+
+end
+
+end
\ No newline at end of file