--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_theorems.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,56 @@
+theory final_theorems
+imports Main rc_theory del_vs_del_s tainted_vs_tainted_s
+begin
+
+context tainting_s_complete begin
+
+theorem static_complete: 
+  assumes undel: "undeletable obj" and tbl: "taintable obj"
+  shows "taintable_s obj"
+proof-
+  from tbl obtain s where tainted: "obj \<in> tainted s"
+    by (auto simp:taintable_def)
+  hence vs: "valid s" by (simp add:tainted_is_valid)
+  from undel vs have "\<not> deleted obj s" and "exists [] obj" 
+    by (auto simp:undeletable_def)
+  moreover from tainted have "valid s" by (rule tainted_is_valid)
+  ultimately have "source_of_sobj (obj2sobj s obj) = Some obj" 
+    using init_obj_keeps_source by auto
+  with tainted t2ts 
+  show ?thesis unfolding taintable_s_def
+    by (rule_tac x = "obj2sobj s obj" in exI, simp)
+qed
+
+theorem undeletable_s_complete:
+  "undeletable_s obj \<Longrightarrow> undeletable obj"
+apply (clarsimp simp:undeletable_s_def undeletable_def)
+apply (drule deleted_imp_deletable_s, simp+)
+done
+
+theorem final_offer:
+  "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; exists [] obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"
+apply (erule swap)
+by (simp add:static_complete undeletable_s_complete)
+
+end
+
+context tainting_s_sound begin
+
+theorem static_sound:
+  assumes tbl_s: "taintable_s obj"
+  shows "taintable obj"
+proof-
+  from tbl_s obtain sobj where ts: "sobj \<in> tainted_s"
+    and sreq: "source_of_sobj sobj = Some obj" 
+    by (auto simp:taintable_s_def)
+  from ts obtain obj' \<tau> where t: "obj' \<in> tainted \<tau>" 
+    and vs: "valid \<tau>" and sreq': "sobj_source_eq_obj sobj obj'"
+    by (auto dest!:tainted_s2tainted dest:tainted_is_valid)
+  from sreq' sreq have "obj = obj'" by (simp add:source_eq)
+  with vs t 
+  show ?thesis by (auto simp:taintable_def)
+qed
+
+end
+
+end
\ No newline at end of file