diff -r e79e3a8a4ceb -r cebdef333899 no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Thu Dec 26 10:56:50 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Mon Dec 30 12:01:09 2013 +0800
@@ -103,14 +103,37 @@
 apply (induct s, simp)
 by (case_tac a, auto)
 
+lemma not_all_msgqs_cons:
+  "p \<notin> all_msgqs (e # s) \<Longrightarrow> p \<notin> all_msgqs s"
+by (case_tac e, auto)
+
+lemma not_all_msgqs_prop:
+  "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p"
+apply (induct s, rule notI, simp)
+apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI)
+apply (case_tac a, auto)
+done
+
+lemma not_all_msgqs_prop2:
+  "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma not_all_msgqs_prop3:
+  "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
 fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
 where
-  "enrich_not_alive s obj (E_file f)  = (f \<notin> current_files s \<and> E_file f \<noteq> obj)"
-| "enrich_not_alive s obj (E_proc p)  = (p \<notin> current_procs s \<and> E_proc p \<noteq> obj)"
-| "enrich_not_alive s obj (E_fd p fd) = ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> E_fd p fd \<noteq> obj)"
-| "enrich_not_alive s obj (E_msgq q)  = (q \<notin> current_msgqs s \<and> E_msgq q \<noteq> obj)"
-| "enrich_not_alive s obj (E_inum i)  = (i \<notin> current_inode_nums s \<and> E_inum i \<noteq> obj)"
-| "enrich_not_alive s obj (E_msg q m) = ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> E_msg q m \<noteq> obj)"
+  "enrich_not_alive s obj (E_file f)  = (f \<notin> current_files s \<and> obj \<noteq> E_file f)"
+| "enrich_not_alive s obj (E_proc p)  = (p \<notin> current_procs s \<and> obj \<noteq> E_proc p)"
+| "enrich_not_alive s obj (E_fd p fd) = 
+  ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> obj \<noteq> E_fd p fd \<and> obj \<noteq> E_proc p)"
+| "enrich_not_alive s obj (E_msgq q)  = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q)"
+| "enrich_not_alive s obj (E_inum i)  = (i \<notin> current_inode_nums s \<and> obj \<noteq> E_inum i)"
+| "enrich_not_alive s obj (E_msg q m) = 
+  ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msg q m \<and> obj \<noteq> E_msgq q)"
 
 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf"
 apply (case_tac f)
@@ -538,7 +561,8 @@
         using os alive' p_in notin_all Open None
         apply (erule_tac x = "E_fd p fd" in allE)
         apply (case_tac obj')
-        by auto
+        apply (auto dest:not_all_procs_prop3)
+        done
       have "os_grant s' e" using p_in f_in fd_not_in os
         by (simp add:Open None)
       moreover have "grant s' e" 
@@ -589,7 +613,7 @@
       have fd_not_in: "fd \<notin> current_proc_fds s' p"
         using os alive' p_in Open Some notin_all
         apply (erule_tac x = "E_fd p fd" in allE)
-        apply (case_tac obj', auto)
+        apply (case_tac obj', auto dest:not_all_procs_prop3)
         done
       have inum_not_in: "inum \<notin> current_inode_nums s'"
         using os alive' Open Some notin_all
@@ -1116,8 +1140,8 @@
       by (simp add:SendMsg)
     have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in
       apply (erule_tac x = "E_msg q m" in allE)
-      apply (case_tac obj')
-      by auto
+      apply (case_tac obj', auto dest:not_all_msgqs_prop3)
+      done
     have "os_grant s' e" using p_in q_in m_not_in
       by (simp add:SendMsg)
     moreover have "grant s' e"