|
1 (*<*) |
|
2 theory Current_files_prop |
|
3 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop |
|
4 begin |
|
5 (*<*) |
|
6 |
|
7 context init begin |
|
8 |
|
9 lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None" |
|
10 by (simp add:current_files_def) |
|
11 |
|
12 (************** file_of_proc_fd vs proc_fd_of_file *****************) |
|
13 lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f" |
|
14 by (simp add:proc_fd_of_file_def) |
|
15 |
|
16 lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f" |
|
17 by (simp add:proc_fd_of_file_def) |
|
18 |
|
19 lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')" |
|
20 by (simp add:proc_fd_of_file_def, auto) |
|
21 |
|
22 lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd" |
|
23 by (drule pfdof_simp3, auto) |
|
24 |
|
25 end |
|
26 |
|
27 context flask begin |
|
28 |
|
29 (***************** inode number lemmas *************************) |
|
30 |
|
31 lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
32 by (auto simp add:current_inode_nums_def current_file_inums_def) |
|
33 |
|
34 lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
35 by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def) |
|
36 |
|
37 lemma fim_noninter_sim_aux[rule_format]: |
|
38 "\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False" |
|
39 apply (induct \<tau>) |
|
40 apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps) |
|
41 apply (drule init_inum_sock_file_noninter, simp, simp) |
|
42 apply ((rule allI|rule impI|erule conjE)+) |
|
43 apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) |
|
44 apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits |
|
45 dest:ios's_im_in_cim iof's_im_in_cim) |
|
46 done |
|
47 |
|
48 lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
49 by (auto intro:fim_noninter_sim_aux) |
|
50 |
|
51 lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
52 by (auto intro:fim_noninter_sim_aux) |
|
53 |
|
54 lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}" |
|
55 by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format]) |
|
56 |
|
57 (******************* file inum has inode tag ************************) |
|
58 |
|
59 lemma finum_has_itag_aux[rule_format]: |
|
60 "\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None" |
|
61 apply (induct \<tau>) |
|
62 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props) |
|
63 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
64 apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def |
|
65 dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits) |
|
66 done |
|
67 |
|
68 lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag" |
|
69 by (auto dest:conjI[THEN finum_has_itag_aux]) |
|
70 |
|
71 (*********************** file inum is file itag *************************) |
|
72 |
|
73 lemma finum_has_ftag_aux[rule_format]: |
|
74 "\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag" |
|
75 apply (induct \<tau>) |
|
76 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props) |
|
77 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
78 apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps |
|
79 split:if_splits option.splits t_socket_type.splits |
|
80 dest:ios's_im_in_cim iof's_im_in_cim) |
|
81 done |
|
82 |
|
83 lemma finum_has_ftag: |
|
84 "\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag" |
|
85 by (auto intro:finum_has_ftag_aux) |
|
86 |
|
87 lemma finum_has_ftag': |
|
88 "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR" |
|
89 apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+) |
|
90 apply (case_tac tag, auto) |
|
91 done |
|
92 |
|
93 (******************* sock inum has inode tag ************************) |
|
94 |
|
95 lemma sinum_has_itag_aux[rule_format]: |
|
96 "\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None" |
|
97 apply (induct \<tau>) |
|
98 apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps) |
|
99 apply (drule init_inumos_prop4, clarsimp) |
|
100 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
101 apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps |
|
102 dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim |
|
103 split:option.splits if_splits t_socket_type.splits) |
|
104 done |
|
105 |
|
106 lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag" |
|
107 by (auto dest:conjI[THEN sinum_has_itag_aux]) |
|
108 |
|
109 (********************** socket inum is socket itag **********************) |
|
110 |
|
111 lemma sinum_has_stag_aux[rule_format]: |
|
112 "\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag" |
|
113 apply (induct \<tau>) |
|
114 apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps) |
|
115 apply (drule init_inumos_prop4, clarsimp) |
|
116 apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a) |
|
117 apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps |
|
118 dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim |
|
119 split:option.splits if_splits t_socket_type.splits) |
|
120 done |
|
121 |
|
122 lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag" |
|
123 by (auto dest:conjI[THEN sinum_has_stag_aux]) |
|
124 |
|
125 lemma sinum_has_stag': |
|
126 "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> |
|
127 \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK" |
|
128 apply (frule sinum_has_itag, simp, erule exE) |
|
129 apply (drule sinum_has_stag, simp+, case_tac tag, simp+) |
|
130 done |
|
131 |
|
132 (************************************ 4 in 1 *************************************) |
|
133 |
|
134 lemma file_leveling: "valid \<tau> \<longrightarrow> ( |
|
135 (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and> |
|
136 (\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and> |
|
137 (\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and> |
|
138 (\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )" |
|
139 proof (induct \<tau>) |
|
140 case Nil |
|
141 show ?case |
|
142 apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits) |
|
143 apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum) |
|
144 apply (rule init_parent_file_has_inum, simp+) |
|
145 apply (rule init_file_has_no_son', simp+) |
|
146 apply (rule init_file_hung_has_no_son, simp+) |
|
147 done |
|
148 next |
|
149 case (Cons a \<tau>) |
|
150 assume pre: "valid \<tau> \<longrightarrow> |
|
151 (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and> |
|
152 (\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and> |
|
153 (\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and> |
|
154 (\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)" |
|
155 show ?case |
|
156 proof |
|
157 assume cons:"valid (a # \<tau>)" |
|
158 show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and> |
|
159 (\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None) \<and> |
|
160 (\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False) \<and> |
|
161 (\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)" |
|
162 proof- |
|
163 have vt: "valid \<tau>" using cons by (auto dest:vd_cons) |
|
164 have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os) |
|
165 have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto |
|
166 have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None" |
|
167 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
168 have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False" |
|
169 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
170 have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False" |
|
171 using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption) |
|
172 have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
173 proof |
|
174 fix f' |
|
175 show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
176 proof (induct f') |
|
177 case Nil show ?case by (auto simp: no_junior_def) |
|
178 next |
|
179 case (Cons a f') |
|
180 assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
181 show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
182 proof clarify |
|
183 fix f im |
|
184 assume h1: "f \<preceq> a # f'" |
|
185 and h2: "inum_of_file \<tau> (a # f') = Some im" |
|
186 show "\<exists>y. inum_of_file \<tau> f = Some y" |
|
187 proof- |
|
188 have h3: "\<exists> y. inum_of_file \<tau> f' = Some y" |
|
189 proof- |
|
190 have "parent (a # f') = Some f'" by simp |
|
191 hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast |
|
192 with h1 show ?thesis by simp |
|
193 qed |
|
194 from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def) |
|
195 moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp |
|
196 moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h3 by simp |
|
197 moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp |
|
198 ultimately show ?thesis by auto |
|
199 qed |
|
200 qed |
|
201 qed |
|
202 qed |
|
203 |
|
204 have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto |
|
205 have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'" |
|
206 using pin by auto |
|
207 have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto |
|
208 have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False" |
|
209 by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def) |
|
210 have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto |
|
211 have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto |
|
212 have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" |
|
213 apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits) |
|
214 by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+) |
|
215 |
|
216 have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None" |
|
217 apply (clarify, case_tac a) using os fin |
|
218 apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def |
|
219 split:if_splits option.splits) |
|
220 done |
|
221 moreover |
|
222 have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" |
|
223 apply (clarify, case_tac a) |
|
224 using vt os pin' |
|
225 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def |
|
226 split:if_splits option.splits t_inode_tag.splits) |
|
227 apply (drule_tac f = pf and f' = f in hns', simp, simp, simp) |
|
228 apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp) |
|
229 apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp) |
|
230 done |
|
231 moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False" |
|
232 apply (clarify, case_tac a) |
|
233 using vt os fns'' cons |
|
234 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps |
|
235 is_file_def is_dir_def |
|
236 dest:ios's_im_in_cim iof's_im_in_cim |
|
237 split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) |
|
238 apply (rule_tac im = a and f = f and f' = f' in fns'', simp+) |
|
239 apply (drule_tac f = f' and pf = list in pin', simp, simp) |
|
240 apply (drule_tac f = f' and pf = list2 in pin', simp, simp) |
|
241 done |
|
242 moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> |
|
243 parent f' = Some f \<longrightarrow> False" |
|
244 apply (clarify, case_tac a) |
|
245 using vt os hns' |
|
246 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps |
|
247 split:if_splits option.splits t_sock_addr.splits) |
|
248 apply (drule fns', simp+) |
|
249 done |
|
250 ultimately show ?thesis by blast |
|
251 qed |
|
252 qed |
|
253 qed |
|
254 |
|
255 (**************** hung file in current ***********************) |
|
256 |
|
257 lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
258 by (drule file_leveling[rule_format], blast) |
|
259 |
|
260 lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" |
|
261 by (auto dest:hung_file_has_inum) |
|
262 |
|
263 lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
264 by (clarsimp simp add:current_files_def hung_file_has_inum') |
|
265 |
|
266 lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None" |
|
267 by (drule file_leveling[rule_format], blast) |
|
268 |
|
269 lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'" |
|
270 by (auto dest:parentf_has_inum) |
|
271 |
|
272 lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
273 by (clarsimp simp add:current_files_def parentf_has_inum') |
|
274 |
|
275 lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
276 apply (subgoal_tac "parent (a # pf) = Some pf") |
|
277 by (erule parentf_in_current, simp+) |
|
278 |
|
279 lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
280 proof (induct f') |
|
281 case Nil show ?case by (auto simp: no_junior_def) |
|
282 next |
|
283 case (Cons a f') |
|
284 assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
285 show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
286 proof clarify |
|
287 fix f im |
|
288 assume h1: "f \<preceq> a # f'" |
|
289 and h2: "inum_of_file \<tau> (a # f') = Some im" |
|
290 and h3: "valid \<tau>" |
|
291 show "\<exists>y. inum_of_file \<tau> f = Some y" |
|
292 proof- |
|
293 have h4: "\<exists> y. inum_of_file \<tau> f' = Some y" |
|
294 proof- |
|
295 have "parent (a # f') = Some f'" by simp |
|
296 hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast |
|
297 with h1 show ?thesis by simp |
|
298 qed |
|
299 from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def) |
|
300 moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp |
|
301 moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp |
|
302 moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp |
|
303 ultimately show ?thesis by auto |
|
304 qed |
|
305 qed |
|
306 qed |
|
307 |
|
308 lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
309 by (rule ancenf_has_inum_aux[rule_format], auto) |
|
310 |
|
311 lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" |
|
312 by (auto dest:ancenf_has_inum) |
|
313 |
|
314 lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
315 by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum') |
|
316 |
|
317 lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
318 by (drule file_leveling[rule_format], blast) |
|
319 |
|
320 lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
321 by (simp add:current_files_def, erule exE, auto intro:file_has_no_son) |
|
322 |
|
323 lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" |
|
324 by (drule file_leveling[rule_format], blast) |
|
325 |
|
326 lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False" |
|
327 by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son) |
|
328 |
|
329 lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False" |
|
330 proof (induct f') |
|
331 case Nil |
|
332 show ?case |
|
333 by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits) |
|
334 next |
|
335 case (Cons a pf) |
|
336 assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False" |
|
337 show ?case |
|
338 proof clarify |
|
339 fix f |
|
340 assume h1: "f \<in> files_hung_by_del \<tau>" |
|
341 and h2: "valid \<tau>" |
|
342 and h3: "a # pf \<in> current_files \<tau>" |
|
343 and h4: "f \<preceq> a # pf" |
|
344 and h5: "f \<noteq> a # pf" |
|
345 have h6: "parent (a # pf) = Some pf" by simp |
|
346 with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
347 from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
348 show False |
|
349 proof (cases "f = pf") |
|
350 case True with h6 h2 h3 h1 |
|
351 show False by (auto intro!:hung_file_no_son') |
|
352 next |
|
353 case False with pre h1 h2 h7 h8 |
|
354 show False by blast |
|
355 qed |
|
356 qed |
|
357 qed |
|
358 |
|
359 lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False" |
|
360 by (rule hung_file_no_des_aux[rule_format], blast) |
|
361 |
|
362 (* current version, dir can not be opened, so hung_files are all files |
|
363 lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f" |
|
364 apply (frule hung_file_has_inum', simp, erule exE) |
|
365 apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits) |
|
366 by (simp add: noJ_Anc, auto dest:hung_file_no_des) |
|
367 *) |
|
368 |
|
369 lemma hung_file_has_filetag: |
|
370 "\<lbrakk>f \<in> files_hung_by_del s; inum_of_file s f = Some im; valid s\<rbrakk> \<Longrightarrow> itag_of_inum s im = Some Tag_FILE" |
|
371 apply (induct s) |
|
372 apply (simp add:files_hung_by_del.simps) |
|
373 apply (drule init_files_hung_prop2, (erule exE)+) |
|
374 apply (drule init_filefd_prop5, clarsimp simp:is_init_file_def split:t_inode_tag.splits option.splits) |
|
375 |
|
376 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
377 apply (auto simp:files_hung_by_del.simps is_file_def is_dir_def current_files_def current_inode_nums_def |
|
378 split:if_splits option.splits t_inode_tag.splits t_socket_type.splits |
|
379 dest:hung_file_has_inum iof's_im_in_cim) |
|
380 done |
|
381 |
|
382 lemma hung_file_is_file: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
|
383 apply (frule hung_file_has_inum', simp, erule exE) |
|
384 apply (drule hung_file_has_filetag, auto simp:is_file_def) |
|
385 done |
|
386 |
|
387 (*********************** 2 in 1 *********************) |
|
388 |
|
389 lemma file_of_pfd_2in1: "valid s \<Longrightarrow> ( |
|
390 (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> inum_of_file s f \<noteq> None) \<and> |
|
391 (\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> is_file s f) )" |
|
392 proof (induct s) |
|
393 case Nil |
|
394 show ?case |
|
395 by (auto dest:init_filefd_valid simp:is_file_def) |
|
396 next |
|
397 case (Cons e s) |
|
398 hence vd_e: "valid (e # s)" and vd_s: "valid s" and os: "os_grant s e" |
|
399 and pfd: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> inum_of_file s f \<noteq> None" |
|
400 and isf: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> is_file s f" |
|
401 by (auto dest:vd_cons vt_grant_os) |
|
402 from pfd have pfd': "\<And> p fd f. inum_of_file s f = None \<Longrightarrow> file_of_proc_fd s p fd \<noteq> Some f" |
|
403 by (rule_tac notI, drule_tac pfd, simp) |
|
404 |
|
405 have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> inum_of_file (e # s) f \<noteq> None" |
|
406 apply (case_tac e) using os |
|
407 apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def |
|
408 dir_is_empty_def is_file_def is_dir_def |
|
409 split:if_splits option.splits dest:pfd) |
|
410 apply (simp add:pfdof_simp3)+ |
|
411 apply (simp add:proc_fd_of_file_def) |
|
412 apply (drule isf, simp add:is_file_def split:t_inode_tag.splits) |
|
413 done |
|
414 moreover |
|
415 have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> is_file (e # s) f" |
|
416 apply (case_tac e) using os |
|
417 apply (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits |
|
418 dest:pfd isf iof's_im_in_cim |
|
419 simp:is_file_def is_dir_def dir_is_empty_def current_files_def) |
|
420 apply (simp add:pfdof_simp3)+ |
|
421 apply (simp add:proc_fd_of_file_def) |
|
422 done |
|
423 ultimately show ?case by auto |
|
424 qed |
|
425 |
|
426 |
|
427 (************** file_of_proc_fd in current ********************) |
|
428 |
|
429 lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
430 by (drule file_of_pfd_2in1, blast) |
|
431 |
|
432 lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" |
|
433 by (auto dest!:file_of_pfd_imp_inode') |
|
434 |
|
435 lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
436 by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def) |
|
437 |
|
438 |
|
439 (*************** file_of_proc_fd is file *********************) |
|
440 |
|
441 lemma file_of_pfd_is_file: |
|
442 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
|
443 by (drule file_of_pfd_2in1, auto simp:is_file_def) |
|
444 |
|
445 lemma file_of_pfd_is_file': |
|
446 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
447 by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
448 |
|
449 lemma file_of_pfd_is_file_tag: |
|
450 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE" |
|
451 by (drule file_of_pfd_is_file, auto simp:is_file_def split:option.splits t_inode_tag.splits) |
|
452 |
|
453 (************** parent file / ancestral file is dir *******************) |
|
454 |
|
455 lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" |
|
456 apply (induct \<tau>) |
|
457 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir') |
|
458 apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a) |
|
459 apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps |
|
460 current_files_def is_dir_def is_file_def |
|
461 dest: ios's_im_in_cim iof's_im_in_cim |
|
462 split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits) |
|
463 apply (drule parentf_has_inum', simp, simp, simp)+ |
|
464 done |
|
465 |
|
466 lemma parentf_has_dirtag: |
|
467 "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk> |
|
468 \<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" |
|
469 by (auto intro:parentf_is_dir_aux[rule_format]) |
|
470 |
|
471 lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
472 apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits) |
|
473 by (auto dest:parentf_has_dirtag) |
|
474 |
|
475 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
476 by (clarsimp simp:current_files_def parentf_is_dir') |
|
477 |
|
478 lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
479 by (auto intro!:parentf_is_dir) |
|
480 |
|
481 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f" |
|
482 proof (induct f') |
|
483 case Nil show ?case |
|
484 by (auto simp:current_files_def no_junior_def) |
|
485 next |
|
486 case (Cons a pf) |
|
487 assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f" |
|
488 show ?case |
|
489 proof clarify |
|
490 fix f |
|
491 assume h1: "f \<preceq> a # pf" |
|
492 and h2: "f \<noteq> a # pf" |
|
493 and h3: "a # pf \<in> current_files \<tau>" |
|
494 and h4: "valid \<tau>" |
|
495 have h5: "parent (a # pf) = Some pf" by simp |
|
496 with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
497 from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
498 show "is_dir \<tau> f" |
|
499 proof (cases "f = pf") |
|
500 case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto) |
|
501 next |
|
502 case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast |
|
503 qed |
|
504 qed |
|
505 qed |
|
506 |
|
507 lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f" |
|
508 by (auto intro:ancenf_is_dir_aux[rule_format]) |
|
509 |
|
510 (************* rebuild current_files simpset ***********************) |
|
511 |
|
512 lemma current_files_nil: "current_files [] = init_files" |
|
513 apply (simp add:current_files_def inum_of_file.simps) |
|
514 by (auto dest:inof_has_file_tag init_file_has_inum) |
|
515 |
|
516 lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)" |
|
517 by (auto simp add:current_files_def inum_of_file.simps split:option.splits) |
|
518 |
|
519 lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>" |
|
520 by (simp add:current_files_def inum_of_file.simps split:option.splits) |
|
521 |
|
522 lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = ( |
|
523 case (file_of_proc_fd \<tau> p fd) of |
|
524 Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>)) |
|
525 then current_files \<tau> - {f} |
|
526 else current_files \<tau>) |
|
527 | _ \<Rightarrow> current_files \<tau> )" |
|
528 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
529 |
|
530 lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)" |
|
531 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
532 |
|
533 lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = current_files \<tau> - {f}" |
|
534 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
535 |
|
536 lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)" |
|
537 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
538 |
|
539 lemma current_files_linkhard: |
|
540 "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)" |
|
541 apply (frule vt_grant_os, frule vd_cons) |
|
542 by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits) |
|
543 |
|
544 (* |
|
545 lemma rename_renaming_decom: |
|
546 "\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f" |
|
547 apply (case_tac "f\<^isub>2 \<preceq> f", simp) |
|
548 apply (simp add:file_after_rename_def split:if_splits) |
|
549 by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current) |
|
550 |
|
551 lemma rename_renaming_decom': |
|
552 "\<lbrakk>\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f" |
|
553 by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+) |
|
554 |
|
555 lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}" |
|
556 apply (frule vt_grant_os, frule vd_cons) |
|
557 apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits) |
|
558 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
559 apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5') |
|
560 apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp) |
|
561 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
562 apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp) |
|
563 apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp) |
|
564 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5) |
|
565 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
566 apply (simp add:file_after_rename_def) |
|
567 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
568 apply (simp add:file_after_rename_def) |
|
569 done |
|
570 *) |
|
571 |
|
572 lemma current_files_other: |
|
573 "\<lbrakk>\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
574 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
575 \<forall> p f. e \<noteq> UnLink p f; |
|
576 \<forall> p f. e \<noteq> Rmdir p f; |
|
577 \<forall> p f i. e \<noteq> Mkdir p f i; |
|
578 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>" |
|
579 by (case_tac e, auto simp:current_files_def inum_of_file.simps) |
|
580 |
|
581 lemmas current_files_simps = current_files_nil current_files_open current_files_open' |
|
582 current_files_closefd current_files_unlink current_files_rmdir |
|
583 current_files_mkdir current_files_linkhard current_files_other |
|
584 |
|
585 |
|
586 (******************** is_file simpset *********************) |
|
587 |
|
588 lemma is_file_open: |
|
589 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
|
590 is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))" |
|
591 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
592 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
593 split:if_splits option.splits t_inode_tag.splits |
|
594 simp:is_file_def current_files_def) |
|
595 done |
|
596 |
|
597 lemma is_file_closefd: |
|
598 "valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = ( |
|
599 case (file_of_proc_fd s p fd) of |
|
600 Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s)) |
|
601 then (is_file s) (f := False) |
|
602 else is_file s) |
|
603 | _ \<Rightarrow> is_file s )" |
|
604 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
605 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
606 split:if_splits option.splits t_inode_tag.splits |
|
607 simp:is_file_def) |
|
608 done |
|
609 |
|
610 lemma is_file_unlink: |
|
611 "valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = ( |
|
612 if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)" |
|
613 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
614 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
615 split:if_splits option.splits t_inode_tag.splits |
|
616 simp:is_file_def) |
|
617 done |
|
618 |
|
619 lemma is_file_linkhard: |
|
620 "valid (LinkHard p f f' # s) \<Longrightarrow> is_file (LinkHard p f f' # s) = (is_file s) (f' := True)" |
|
621 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
622 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
623 split:if_splits option.splits t_inode_tag.splits |
|
624 simp:is_file_def) |
|
625 done |
|
626 |
|
627 lemma is_file_other: |
|
628 "\<lbrakk>valid (e # \<tau>); |
|
629 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
630 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
631 \<forall> p f. e \<noteq> UnLink p f; |
|
632 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> is_file (e # \<tau>) = is_file \<tau>" |
|
633 apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e) |
|
634 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
635 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
636 simp:is_file_def dir_is_empty_def is_dir_def current_files_def) |
|
637 done |
|
638 |
|
639 lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False" |
|
640 by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
641 |
|
642 lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f" |
|
643 by (rule notI, erule file_dir_conflict, simp) |
|
644 |
|
645 lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f" |
|
646 by (rule notI, erule file_dir_conflict, simp) |
|
647 |
|
648 lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other |
|
649 |
|
650 (********* is_dir simpset **********) |
|
651 |
|
652 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)" |
|
653 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
654 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
655 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
656 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
657 done |
|
658 |
|
659 lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)" |
|
660 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
661 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
662 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
663 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
664 done |
|
665 |
|
666 lemma is_dir_other: |
|
667 "\<lbrakk>valid (e # s); |
|
668 \<forall> p f. e \<noteq> Rmdir p f; |
|
669 \<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s" |
|
670 apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e) |
|
671 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
672 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
673 simp:is_file_def dir_is_empty_def is_dir_def current_files_def) |
|
674 apply (drule file_of_pfd_is_file, simp) |
|
675 apply (simp add:is_file_def split:t_inode_tag.splits option.splits) |
|
676 done |
|
677 |
|
678 lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other |
|
679 |
|
680 (*********** no root dir involved ***********) |
|
681 |
|
682 lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []" |
|
683 apply (induct s, simp add:is_dir_nil root_is_init_dir) |
|
684 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
685 apply (auto simp:is_dir_simps) |
|
686 done |
|
687 |
|
688 lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False" |
|
689 apply (drule root_is_dir) |
|
690 apply (erule file_dir_conflict, simp) |
|
691 done |
|
692 |
|
693 lemma noroot_execve: |
|
694 "valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []" |
|
695 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
696 |
|
697 lemma noroot_execve': |
|
698 "valid (Execve p [] fds # s) \<Longrightarrow> False" |
|
699 by (drule noroot_execve, simp) |
|
700 |
|
701 lemma noroot_open: |
|
702 "valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []" |
|
703 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits) |
|
704 |
|
705 lemma noroot_open': |
|
706 "valid (Open p [] flags fd opt # s) \<Longrightarrow> False" |
|
707 by (drule noroot_open, simp) |
|
708 |
|
709 lemma noroot_filefd': |
|
710 "\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False" |
|
711 apply (induct s arbitrary:p, simp) |
|
712 apply (drule init_filefd_prop5, erule root_is_init_dir') |
|
713 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
714 apply (auto split:if_splits option.splits dest!:root_is_dir') |
|
715 done |
|
716 |
|
717 lemma noroot_filefd: |
|
718 "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []" |
|
719 by (rule notI, simp, erule noroot_filefd', simp) |
|
720 |
|
721 lemma noroot_unlink: |
|
722 "valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []" |
|
723 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
724 |
|
725 lemma noroot_unlink': |
|
726 "valid (UnLink p [] # s) \<Longrightarrow> False" |
|
727 by (drule noroot_unlink, simp) |
|
728 |
|
729 lemma noroot_rmdir: |
|
730 "valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []" |
|
731 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
732 |
|
733 lemma noroot_rmdir': |
|
734 "valid (Rmdir p [] # s) \<Longrightarrow> False" |
|
735 by (drule noroot_rmdir, simp) |
|
736 |
|
737 lemma noroot_mkdir: |
|
738 "valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []" |
|
739 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
740 |
|
741 lemma noroot_mkdir': |
|
742 "valid (Mkdir p [] inum # s) \<Longrightarrow> False" |
|
743 by (drule noroot_mkdir, simp) |
|
744 |
|
745 lemma noroot_linkhard: |
|
746 "valid (LinkHard p f f' # s) \<Longrightarrow> f \<noteq> [] \<and> f' \<noteq> []" |
|
747 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
748 |
|
749 lemma noroot_linkhard': |
|
750 "valid (LinkHard p [] f # s) \<Longrightarrow> False" |
|
751 by (drule noroot_linkhard, simp) |
|
752 |
|
753 lemma noroot_linkhard'': |
|
754 "valid (LinkHard p f [] # s) \<Longrightarrow> False" |
|
755 by (drule noroot_linkhard, simp) |
|
756 |
|
757 lemma noroot_truncate: |
|
758 "valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []" |
|
759 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
760 |
|
761 lemma noroot_truncate': |
|
762 "valid (Truncate p [] len # s) \<Longrightarrow> False" |
|
763 by (drule noroot_truncate, simp) |
|
764 |
|
765 lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir |
|
766 noroot_mkdir noroot_linkhard noroot_truncate |
|
767 |
|
768 lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir' |
|
769 noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate' |
|
770 |
|
771 |
|
772 lemma is_file_in_current: |
|
773 "is_file s f \<Longrightarrow> f \<in> current_files s" |
|
774 by (auto simp:is_file_def current_files_def split:option.splits) |
|
775 |
|
776 lemma is_dir_in_current: |
|
777 "is_dir s f \<Longrightarrow> f \<in> current_files s" |
|
778 by (auto simp:is_dir_def current_files_def split:option.splits) |
|
779 |
|
780 |
|
781 (* simpset for same_inode_files: Current_files_prop.thy *) |
|
782 |
|
783 lemma same_inode_files_nil: |
|
784 "same_inode_files [] = init_same_inode_files" |
|
785 by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil) |
|
786 |
|
787 lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>" |
|
788 by (auto simp add:current_inode_nums_def current_file_inums_def) |
|
789 |
|
790 lemma same_inode_files_open: |
|
791 "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'. |
|
792 if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')" |
|
793 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
794 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits |
|
795 dest:iof's_im_in_cim iof's_im_in_cim') |
|
796 apply (drule is_file_in_current) |
|
797 apply (simp add:current_files_def) |
|
798 done |
|
799 |
|
800 lemma same_inode_files_linkhard: |
|
801 "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. |
|
802 if (f' = f \<or> f' \<in> same_inode_files s oldf) |
|
803 then same_inode_files s oldf \<union> {f} |
|
804 else same_inode_files s f')" |
|
805 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
806 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits |
|
807 dest:iof's_im_in_cim iof's_im_in_cim') |
|
808 apply (drule is_file_in_current) |
|
809 apply (simp add:current_files_def is_file_def) |
|
810 apply (simp add:is_file_def) |
|
811 done |
|
812 |
|
813 lemma inum_of_file_none_prop: |
|
814 "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s" |
|
815 by (simp add:current_files_def) |
|
816 |
|
817 lemma same_inode_files_closefd: |
|
818 "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> |
|
819 same_inode_files (CloseFd p fd # s) f' = ( |
|
820 case (file_of_proc_fd s p fd) of |
|
821 Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s)) |
|
822 then same_inode_files s f' - {f} |
|
823 else same_inode_files s f' ) |
|
824 | None \<Rightarrow> same_inode_files s f' )" |
|
825 apply (frule vt_grant_os, frule vd_cons) |
|
826 apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd |
|
827 split:if_splits option.splits |
|
828 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop) |
|
829 done |
|
830 |
|
831 lemma same_inode_files_unlink: |
|
832 "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> |
|
833 \<Longrightarrow> same_inode_files (UnLink p f # s) f' = ( |
|
834 if (proc_fd_of_file s f = {}) |
|
835 then same_inode_files s f' - {f} |
|
836 else same_inode_files s f')" |
|
837 apply (frule vt_grant_os, frule vd_cons) |
|
838 apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink |
|
839 split:if_splits option.splits |
|
840 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop) |
|
841 done |
|
842 |
|
843 lemma same_inode_files_mkdir: |
|
844 "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)" |
|
845 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
846 apply (auto simp:same_inode_files_def is_file_simps current_files_simps |
|
847 split:if_splits option.splits |
|
848 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current) |
|
849 apply (simp add:current_files_def is_file_def) |
|
850 done |
|
851 |
|
852 lemma same_inode_files_other: |
|
853 "\<lbrakk>valid (e # s); |
|
854 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
855 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
856 \<forall> p f. e \<noteq> UnLink p f; |
|
857 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s) = same_inode_files s" |
|
858 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e) |
|
859 apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def |
|
860 split:if_splits option.splits |
|
861 dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir) |
|
862 apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+ |
|
863 done |
|
864 |
|
865 lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard |
|
866 same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other |
|
867 |
|
868 lemma same_inode_files_prop1: |
|
869 "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s" |
|
870 by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits) |
|
871 |
|
872 lemma same_inode_files_prop2: |
|
873 "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''" |
|
874 by (auto dest:same_inode_files_prop1) |
|
875 |
|
876 lemma same_inode_files_prop3: |
|
877 "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''" |
|
878 apply (rule notI) |
|
879 apply (simp add:same_inode_files_def is_file_def is_dir_def |
|
880 split:if_splits option.splits t_inode_tag.splits) |
|
881 done |
|
882 |
|
883 lemma same_inode_files_prop4: |
|
884 "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f" |
|
885 by (auto simp:same_inode_files_def split:if_splits) |
|
886 |
|
887 lemma same_inode_files_prop5: |
|
888 "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'" |
|
889 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
890 |
|
891 lemma same_inode_files_prop6: |
|
892 "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f" |
|
893 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
894 |
|
895 lemma same_inode_files_prop7: |
|
896 "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'" |
|
897 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
898 |
|
899 lemma same_inode_files_prop8: |
|
900 "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f" |
|
901 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
902 |
|
903 |
|
904 end |
|
905 |
|
906 end |