--- a/Tainted_prop.thy	Sun Jun 16 08:05:37 2013 +0800
+++ b/Tainted_prop.thy	Mon Jun 24 09:01:42 2013 +0800
@@ -95,6 +95,13 @@
 (*?? need simpset for tainted *)
 sorry
 
+lemma info_flow_shm_intro:
+  "\<lbrakk>(p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h; valid s\<rbrakk>
+   \<Longrightarrow> info_flow_shm s p p'"
+apply (rule_tac p = p and p' = p in info_flow_shm.intros(2))
+apply (auto intro!:info_flow_shm.intros(1) procs_of_shm_prop2)
+done
+
 lemma info_flow_shm_Tainted:
   "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
 proof (induct s arbitrary:p p')
@@ -109,7 +116,7 @@
   have p4': 
     "\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk> 
                 \<Longrightarrow> O_proc p' \<in> Tainted s"
-    by (rule p4, auto simp:info_flow_shm_def)    
+    by (rule p4, auto intro!:info_flow_shm_intro p5)    
   from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)"
     by (auto dest:info_shm_flow_in_procs)
   show ?case
@@ -120,8 +127,12 @@
     with p1 p2 p5 p6 p7 p8 p3 show ?thesis
     apply (case_tac e)
     prefer 7
-    apply (simp add:info_flow_shm_def split:if_splits option.splits)
+    apply (simp split:if_splits option.splits)
     apply (rule allI|rule impI|rule conjI)+
+
+
+    apply (auto dest:p4'   procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]
+
     apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)
     apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)
     apply ((erule exE|erule conjE)+)