Flask.thy
changeset 14 cc1e46225a81
parent 13 7b5e9fbeaf93
child 15 4ca824cd0c59
--- 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>) =