--- a/Tainted_prop.thy	Thu Jul 11 07:52:06 2013 +0800
+++ b/Tainted_prop.thy	Thu Aug 01 12:19:42 2013 +0800
@@ -1,5 +1,5 @@
 theory Tainted_prop 
-imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop 
 begin
 
 context tainting begin
@@ -80,7 +80,7 @@
 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits
            intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 
             dest:info_shm_flow_in_procs)
-done
+done 
 
 lemma Tainted_proc_in_current:
   "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
@@ -102,6 +102,11 @@
 (*?? need simpset for tainted *)
 sorry
 
+lemma "\<lbrakk>info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\<rbrakk> \<Longrightarrow> info_flow_shm s pa pc"
+apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2)
+apply (erule_tac x = h in allE, simp)
+apply (case_tac "h = ha", simp+)
+sorry
 
 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"
@@ -117,9 +122,10 @@
   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 one_flow_shm_def)    
-  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)
+    apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *)    
+    sorry
+  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) *) sorry
   show ?case
   proof (cases "self_shm s p p'")
     case True with p1 show ?thesis by simp