--- a/Flask.thy Thu May 30 09:15:19 2013 +0800
+++ b/Flask.thy Thu May 30 15:28:57 2013 +0800
@@ -157,6 +157,7 @@
and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"
and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"
+ and init_procshm_valid: "\<And> p h flag flag'. \<lbrakk>(p,flag) \<in> init_procs_of_shm h; (p, flag') \<in> init_procs_of_shm h\<rbrakk> \<Longrightarrow> flag = flag'"
and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)"
and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
@@ -426,7 +427,7 @@
| "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"
| "current_shms (e # \<tau>) = current_shms \<tau> "
-fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
+fun procs_of_shm : "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
where
"procs_of_shm [] = init_procs_of_shm"
| "procs_of_shm (CreateShM p h # \<tau>) =