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