|
1
|
1 |
theory Deleted_prop
|
|
4
|
2 |
imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop
|
|
1
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
context flask begin
|
|
|
6 |
|
|
|
7 |
lemma deleted_cons_I: "deleted obj s \<Longrightarrow> deleted obj (e # s)"
|
|
|
8 |
by (case_tac e, auto)
|
|
|
9 |
|
|
|
10 |
lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s"
|
|
|
11 |
by (auto dest:deleted_cons_I)
|
|
|
12 |
|
|
4
|
13 |
lemma not_deleted_init_file:
|
|
|
14 |
"\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
|
|
|
15 |
apply (induct s, simp add:is_init_file_prop1)
|
|
|
16 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
17 |
apply (case_tac a) prefer 6 apply (case_tac option)
|
|
|
18 |
apply (auto simp:is_file_simps split:option.splits)
|
|
|
19 |
done
|
|
|
20 |
|
|
|
21 |
lemma not_deleted_init_dir:
|
|
|
22 |
"\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"
|
|
|
23 |
apply (induct s, simp add:is_init_dir_prop1)
|
|
|
24 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
25 |
apply (case_tac a) prefer 6 apply (case_tac option)
|
|
|
26 |
apply (auto simp:is_dir_simps split:option.splits)
|
|
|
27 |
done
|
|
|
28 |
|
|
|
29 |
lemma not_deleted_init_proc:
|
|
|
30 |
"\<lbrakk>\<not> deleted (O_proc p) s; p \<in> init_procs\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
|
|
|
31 |
apply (induct s, simp)
|
|
|
32 |
by (case_tac a, auto)
|
|
|
33 |
|
|
|
34 |
(**** ???*)
|
|
|
35 |
lemma current_fd_imp_current_proc:
|
|
|
36 |
"\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
|
|
|
37 |
apply (induct s)
|
|
|
38 |
apply (simp add:init_fds_of_proc_prop1)
|
|
|
39 |
apply (frule vd_cons, drule vt_grant_os, case_tac a)
|
|
|
40 |
by (auto split:if_splits option.splits)
|
|
|
41 |
|
|
|
42 |
lemma not_deleted_init_fd_aux:
|
|
|
43 |
"\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk>
|
|
|
44 |
\<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> deleted (O_proc p) s"
|
|
|
45 |
apply (induct s arbitrary: p, simp)
|
|
|
46 |
apply (frule vd_cons, drule vt_grant_os)
|
|
|
47 |
apply (case_tac a, auto dest:current_fd_imp_current_proc)
|
|
|
48 |
done
|
|
|
49 |
|
|
|
50 |
lemma not_deleted_init_fd2:
|
|
|
51 |
"\<lbrakk>\<not> deleted (O_fd p fd) s; fd \<in> init_fds_of_proc p; valid s\<rbrakk> \<Longrightarrow> \<not> deleted (O_proc p) s"
|
|
|
52 |
by (auto dest:not_deleted_init_fd_aux)
|
|
|
53 |
|
|
|
54 |
lemma not_deleted_init_fd1:
|
|
|
55 |
"\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
|
|
|
56 |
by (auto dest:not_deleted_init_fd_aux)
|
|
|
57 |
|
|
|
58 |
lemma not_deleted_init_tcp_aux:
|
|
|
59 |
"\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk>
|
|
|
60 |
\<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
|
|
|
61 |
apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1)
|
|
|
62 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
63 |
apply (case_tac a) prefer 6 apply (case_tac option)
|
|
|
64 |
by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits
|
|
|
65 |
dest:is_tcp_sock_imp_curernt_proc)
|
|
|
66 |
|
|
|
67 |
lemma not_deleted_init_tcp1:
|
|
|
68 |
"\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk>
|
|
|
69 |
\<Longrightarrow> is_tcp_sock s (p,fd)"
|
|
|
70 |
by (auto dest:not_deleted_init_tcp_aux)
|
|
|
71 |
|
|
|
72 |
lemma not_deleted_init_tcp2:
|
|
|
73 |
"\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk>
|
|
|
74 |
\<Longrightarrow> \<not> deleted (O_proc p) s"
|
|
|
75 |
by (auto dest:not_deleted_init_tcp_aux)
|
|
|
76 |
|
|
|
77 |
lemma not_deleted_init_udp_aux:
|
|
|
78 |
"\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk>
|
|
|
79 |
\<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
|
|
|
80 |
apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1)
|
|
|
81 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
82 |
apply (case_tac a) prefer 6 apply (case_tac option)
|
|
|
83 |
by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits
|
|
|
84 |
dest:is_udp_sock_imp_curernt_proc)
|
|
|
85 |
|
|
|
86 |
lemma not_deleted_init_udp1:
|
|
|
87 |
"\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk>
|
|
|
88 |
\<Longrightarrow> is_udp_sock s (p,fd)"
|
|
|
89 |
by (auto dest:not_deleted_init_udp_aux)
|
|
|
90 |
|
|
|
91 |
lemma not_deleted_init_udp2:
|
|
|
92 |
"\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk>
|
|
|
93 |
\<Longrightarrow> \<not> deleted (O_proc p) s"
|
|
|
94 |
by (auto dest:not_deleted_init_udp_aux)
|
|
|
95 |
|
|
|
96 |
lemma not_deleted_init_shm:
|
|
|
97 |
"\<lbrakk>\<not> deleted (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
|
|
|
98 |
apply (induct s, simp)
|
|
|
99 |
by (case_tac a, auto)
|
|
|
100 |
|
|
|
101 |
lemma not_deleted_init_msgq:
|
|
|
102 |
"\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
|
|
|
103 |
apply (induct s, simp)
|
|
|
104 |
by (case_tac a, auto)
|
|
|
105 |
|
|
|
106 |
lemma current_msg_imp_current_msgq:
|
|
|
107 |
"\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
|
|
|
108 |
apply (induct s)
|
|
|
109 |
apply (simp add:init_msgs_valid)
|
|
|
110 |
apply (frule vd_cons, drule vt_grant_os)
|
|
|
111 |
apply (case_tac a, auto split:if_splits)
|
|
|
112 |
done
|
|
|
113 |
|
|
|
114 |
lemma not_deleted_init_msg:
|
|
|
115 |
"\<lbrakk>\<not> deleted (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"
|
|
|
116 |
apply (induct s, simp)
|
|
|
117 |
apply (frule vd_cons, frule vt_grant_os)
|
|
|
118 |
apply (case_tac a, auto dest:current_msg_imp_current_msgq)
|
|
|
119 |
apply (case_tac "msgs_of_queue s q", simp+)
|
|
|
120 |
done
|
|
|
121 |
|
|
|
122 |
lemma not_deleted_imp_alive:
|
|
1
|
123 |
"\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
|
|
4
|
124 |
apply (case_tac obj)
|
|
|
125 |
apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc
|
|
|
126 |
not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm
|
|
|
127 |
not_deleted_init_msgq
|
|
|
128 |
intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current
|
|
|
129 |
current_msg_imp_current_msgq)
|
|
1
|
130 |
done
|
|
|
131 |
|
|
|
132 |
lemma cons_app_simp_aux:
|
|
|
133 |
"(a # b) @ c = a # (b @ c)" by auto
|
|
|
134 |
|
|
4
|
135 |
lemma not_deleted_imp_alive_app:
|
|
|
136 |
"\<lbrakk>\<not> deleted obj (s'@s); alive s obj\<rbrakk> \<Longrightarrow> alive (s'@s) obj"
|
|
1
|
137 |
apply (induct s', simp, simp only:cons_app_simp_aux)
|
|
4
|
138 |
apply (frule not_deleted_cons_D, simp)
|
|
1
|
139 |
apply (case_tac a, case_tac [!] obj, auto)
|
|
|
140 |
done
|
|
|
141 |
|
|
|
142 |
(*
|
|
|
143 |
|
|
|
144 |
lemma nodel_imp_un_deleted:
|
|
|
145 |
"no_del_event s \<Longrightarrow> \<not> deleted obj s"
|
|
|
146 |
by (induct s, simp, case_tac a,auto)
|
|
|
147 |
|
|
|
148 |
lemma nodel_exists_remains:
|
|
|
149 |
"\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"
|
|
|
150 |
apply (drule_tac obj = obj in nodel_imp_un_deleted)
|
|
|
151 |
by (simp add:not_deleted_imp_exists')
|
|
|
152 |
|
|
|
153 |
lemma nodel_imp_exists:
|
|
|
154 |
"\<lbrakk>no_del_event s; exists [] obj\<rbrakk> \<Longrightarrow> exists s obj"
|
|
|
155 |
apply (drule_tac obj = obj in nodel_imp_un_deleted)
|
|
|
156 |
by (simp add:not_deleted_imp_exists)
|
|
|
157 |
|
|
|
158 |
lemma no_del_event_cons_D:
|
|
|
159 |
"no_del_event (e # s) \<Longrightarrow> no_del_event s"
|
|
|
160 |
by (case_tac e, auto)
|
|
|
161 |
*)
|
|
|
162 |
end
|
|
|
163 |
|
|
|
164 |
end |