(*<*)+
−
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_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')+
−
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+
−
+
−
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"+
−
by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)+
−
+
−
lemma flag_of_proc_shm_prop1:+
−
  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"+
−
apply (induct s arbitrary:p flag)+
−
apply (simp, drule init_shmflag_has_proc, 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 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"+
−
by (auto simp add:has_same_inode_def current_files_def)+
−
+
−
lemma has_same_inode_prop1:+
−
  "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"+
−
by (auto simp:has_same_inode_def is_file_def)+
−
+
−
lemma has_same_inode_prop1':+
−
  "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"+
−
by (auto simp:has_same_inode_def is_file_def)+
−
+
−
lemma has_same_inode_prop2:+
−
  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"+
−
apply (drule has_same_inode_prop1)+
−
apply (simp add:file_of_pfd_is_file, simp+)+
−
done+
−
+
−
lemma has_same_inode_prop2':+
−
  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"+
−
apply (drule has_same_inode_prop1')+
−
apply (simp add:file_of_pfd_is_file, simp+)+
−
done+
−
+
−
lemma tobj_in_init_alive:+
−
  "tobj_in_init obj \<Longrightarrow> init_alive obj"+
−
by (case_tac obj, auto)+
−
+
−
lemma tobj_in_alive:+
−
  "tobj_in_init obj \<Longrightarrow> alive [] obj"+
−
by (case_tac obj, auto simp:is_file_nil)+
−
+
−
end+
−
+
−
end+
−