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