|
19
|
1 |
(*<*)
|
|
18
|
2 |
theory Current_prop
|
|
|
3 |
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
|
|
|
4 |
begin
|
|
19
|
5 |
(*>*)
|
|
18
|
6 |
|
|
|
7 |
context flask begin
|
|
|
8 |
|
|
|
9 |
lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
|
|
|
10 |
apply (induct s arbitrary:p_flag)
|
|
|
11 |
apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
|
|
|
12 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
13 |
apply (case_tac a, auto split:if_splits option.splits)
|
|
|
14 |
done
|
|
|
15 |
|
|
|
16 |
lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
|
|
|
17 |
apply (induct s arbitrary:p flag)
|
|
|
18 |
apply (simp, drule init_procs_has_shm, simp)
|
|
|
19 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
20 |
apply (case_tac a, auto split:if_splits option.splits)
|
|
|
21 |
done
|
|
|
22 |
|
|
|
23 |
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>
|
|
|
24 |
\<Longrightarrow> flag = flag'"
|
|
|
25 |
apply (induct s arbitrary:p flag flag')
|
|
|
26 |
apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
|
|
|
27 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
28 |
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
|
|
|
29 |
done
|
|
|
30 |
|
|
|
31 |
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"
|
|
|
32 |
apply (induct s arbitrary:p flag)
|
|
|
33 |
apply (simp, drule init_procs_has_shm, simp)
|
|
|
34 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
35 |
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
|
|
|
36 |
done
|
|
|
37 |
|
|
|
38 |
lemma procs_of_shm_prop4':
|
|
|
39 |
"\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
|
|
|
40 |
by (auto dest:procs_of_shm_prop4)
|
|
|
41 |
|
|
|
42 |
lemma not_init_intro_proc:
|
|
|
43 |
"\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
|
|
|
44 |
using not_deleted_init_proc by auto
|
|
|
45 |
|
|
|
46 |
lemma not_init_intro_proc':
|
|
|
47 |
"\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
|
|
|
48 |
using not_deleted_init_proc by auto
|
|
|
49 |
|
|
19
|
50 |
lemma has_same_inode_in_current:
|
|
|
51 |
"\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
|
|
|
52 |
by (auto simp add:has_same_inode_def current_files_def)
|
|
|
53 |
|
|
|
54 |
lemma has_same_inode_prop1:
|
|
|
55 |
"\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
|
|
|
56 |
by (auto simp:has_same_inode_def is_file_def)
|
|
|
57 |
|
|
|
58 |
lemma has_same_inode_prop1':
|
|
|
59 |
"\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
|
|
|
60 |
by (auto simp:has_same_inode_def is_file_def)
|
|
|
61 |
|
|
|
62 |
lemma has_same_inode_prop2:
|
|
|
63 |
"\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
|
|
|
64 |
apply (drule has_same_inode_prop1)
|
|
|
65 |
apply (simp add:file_of_pfd_is_file, simp+)
|
|
|
66 |
done
|
|
|
67 |
|
|
|
68 |
lemma has_same_inode_prop2':
|
|
|
69 |
"\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
|
|
|
70 |
apply (drule has_same_inode_prop1')
|
|
|
71 |
apply (simp add:file_of_pfd_is_file, simp+)
|
|
|
72 |
done
|
|
|
73 |
|
|
|
74 |
lemma tobj_in_init_alive:
|
|
|
75 |
"tobj_in_init obj \<Longrightarrow> init_alive obj"
|
|
|
76 |
by (case_tac obj, auto)
|
|
|
77 |
|
|
|
78 |
lemma tobj_in_alive:
|
|
|
79 |
"tobj_in_init obj \<Longrightarrow> alive [] obj"
|
|
|
80 |
by (case_tac obj, auto simp:is_file_nil)
|
|
|
81 |
|
|
18
|
82 |
end
|
|
|
83 |
|
|
|
84 |
end |