diff -r 924ab7a4e7fa -r 271e9818b6f6 Final_theorem.thy
--- a/Final_theorem.thy	Wed Nov 20 21:33:56 2013 +0800
+++ b/Final_theorem.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -67,6 +67,7 @@
     apply (simp add:init_ss_eq_def)
     apply (rule_tac x = "ss'" in bexI)
     apply (rule_tac x = "sobj" in exI)
+    thm tainted_s_subset_prop
     by (auto intro:tainted_s_subset_prop)
 qed
 
@@ -186,6 +187,43 @@
 
 declare co2sobj.simps [simp add]
 
+lemma subseteq_D:
+  "\<lbrakk> S \<subseteq> {x. P x}; x \<in> S\<rbrakk> \<Longrightarrow> P x"
+by auto
+
+lemma "\<lbrakk>tainted_s ss sobj; ss \<in> static; is_init_sobj sobj\<rbrakk> 
+   \<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+apply (drule s2d_main')
+apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE)
+apply (rule_tac x = s in exI, simp)
+apply (case_tac sobj, simp_all only:tainted_s.simps)
+thm set_eq_D
+apply (simp split:option.splits)
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+
+lemma tainted_s_imp_tainted:
+  "\<lbrakk>tainted_s ss sobj; ss \<in> static; init_obj_related sobj obj\<rbrakk> 
+   \<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+apply (drule s2d_main')
+apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE)
+apply (rule_tac x = s in exI, simp)
+apply (case_tac sobj, simp_all)
+apply (case_tac[!] obj, simp_all del:co2sobj.simps)
+apply (simp split:option.splits)
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+sorry
+
+
+
+
 lemma tainted_s_imp_tainted:
   "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
 apply (drule s2d_main)