--- a/Current_prop.thy	Mon Jun 24 09:01:42 2013 +0800
+++ b/Current_prop.thy	Mon Jun 24 15:22:37 2013 +0800
@@ -20,6 +20,10 @@
 apply (case_tac a, auto split:if_splits option.splits)
 done
 
+lemma procs_of_shm_prop2':
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<forall> flag h. (p, flag) \<notin> procs_of_shm s h"
+by (auto dest:procs_of_shm_prop2)
+
 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
   \<Longrightarrow> flag = flag'"
 apply (induct s arbitrary:p flag flag')
@@ -49,11 +53,77 @@
 
 lemma info_shm_flow_in_procs:
   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
-apply (induct rule:info_flow_shm.induct )
-by (auto intro:procs_of_shm_prop2)
+by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
 
 (*********** simpset for info_flow_shm **************)
 
+lemma info_flow_shm_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
+     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
+     (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+     (info_flow_shm s pa pb)                       )"
+apply (rule ext, rule ext, frule vt_grant_os)
+by (auto simp add:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_detach:
+  "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 
+     self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
+     (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
+apply (rule ext, rule ext, frule vt_grant_os)
+by (auto simp:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. 
+     self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)     )"
+apply (rule ext, rule ext, frule vt_grant_os)
+by (auto simp:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb. 
+     (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> 
+     (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> 
+     (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
+apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+apply (auto simp:info_flow_shm_def one_flow_shm_def)
+done
+
+lemma info_flow_shm_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 
+     (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb)    )"
+apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. 
+     pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb                 )"
+apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_exit:
+  "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. 
+     pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb                          )"
+apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:info_flow_shm_def one_flow_shm_def)
+
+lemma info_flow_shm_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p
+   \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"
+apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)
+apply (erule_tac x = h in allE, simp)
+apply (drule procs_of_shm_prop1, auto)
+done
+
+
+(*
 lemma info_flow_shm_prop1: 
   "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 
    \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
@@ -83,10 +153,15 @@
 where
   "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
 
+inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"
+
 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
 where
   "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
-| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. if (p' = p) then {p''. \<exists> }"
+| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. 
+     if (p' = p) then flowed_procs s h 
+     else if ()
+    "
 
 
 lemma info_flow_shm_attach:
@@ -107,8 +182,9 @@
 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
 apply (rule notI, erule info_flow_shm.cases, simp+)
 pr 5
-
-lemmas info_flow_shm_simps = info_flow_shm_other
+*)
+lemmas info_flow_shm_simps = info_flow_shm_other info_flow_shm_attach info_flow_shm_detach info_flow_shm_deleteshm
+  info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit
 
 lemma has_same_inode_in_current:
   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"