diff -r 570f90f175ee -r 9b42765ce554 Current_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Current_prop.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -0,0 +1,51 @@
+theory Current_prop
+imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
+begin
+(*<*)
+
+context flask begin
+
+lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
+apply (induct s arbitrary:p_flag)
+apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
+lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
+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')
+apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
+done
+
+lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_procs_has_shm, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
+done
+
+lemma procs_of_shm_prop4':
+  "\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
+by (auto dest:procs_of_shm_prop4)
+
+lemma not_init_intro_proc:
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
+using not_deleted_init_proc by auto
+
+lemma not_init_intro_proc':
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
+using not_deleted_init_proc by auto
+
+end
+
+end
\ No newline at end of file