|
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 |
|
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 split:if_splits option.splits) |
|
226 apply (drule_tac f = pf and f' = f in hns', simp, simp, simp) |
|
227 apply (drule_tac f = list and f' = f in fns', simp, simp, simp) |
|
228 apply (drule_tac f = list and f' = f in dns', simp, simp, simp) |
|
229 done |
|
230 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" |
|
231 apply (clarify, case_tac a) |
|
232 using vt os fns'' |
|
233 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps |
|
234 is_file_def is_dir_def |
|
235 dest:ios's_im_in_cim iof's_im_in_cim |
|
236 split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) |
|
237 apply (drule_tac f = f' and pf = list in pin', simp, simp) |
|
238 apply (drule_tac f = f' and pf = list2 in pin', simp, simp) |
|
239 done |
|
240 moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> |
|
241 parent f' = Some f \<longrightarrow> False" |
|
242 apply (clarify, case_tac a) |
|
243 using vt os hns' |
|
244 apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps |
|
245 split:if_splits option.splits t_sock_addr.splits) |
|
246 apply (drule fns', simp+) |
|
247 done |
|
248 ultimately show ?thesis by blast |
|
249 qed |
|
250 qed |
|
251 qed |
|
252 |
|
253 (**************** hung file in current ***********************) |
|
254 |
|
255 lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
256 by (drule file_leveling[rule_format], blast) |
|
257 |
|
258 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" |
|
259 by (auto dest:hung_file_has_inum) |
|
260 |
|
261 lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
262 by (clarsimp simp add:current_files_def hung_file_has_inum') |
|
263 |
|
264 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" |
|
265 by (drule file_leveling[rule_format], blast) |
|
266 |
|
267 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'" |
|
268 by (auto dest:parentf_has_inum) |
|
269 |
|
270 lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
271 by (clarsimp simp add:current_files_def parentf_has_inum') |
|
272 |
|
273 lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>" |
|
274 apply (subgoal_tac "parent (a # pf) = Some pf") |
|
275 by (erule parentf_in_current, simp+) |
|
276 |
|
277 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" |
|
278 proof (induct f') |
|
279 case Nil show ?case by (auto simp: no_junior_def) |
|
280 next |
|
281 case (Cons a f') |
|
282 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" |
|
283 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" |
|
284 proof clarify |
|
285 fix f im |
|
286 assume h1: "f \<preceq> a # f'" |
|
287 and h2: "inum_of_file \<tau> (a # f') = Some im" |
|
288 and h3: "valid \<tau>" |
|
289 show "\<exists>y. inum_of_file \<tau> f = Some y" |
|
290 proof- |
|
291 have h4: "\<exists> y. inum_of_file \<tau> f' = Some y" |
|
292 proof- |
|
293 have "parent (a # f') = Some f'" by simp |
|
294 hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast |
|
295 with h1 show ?thesis by simp |
|
296 qed |
|
297 from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def) |
|
298 moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp |
|
299 moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp |
|
300 moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp |
|
301 ultimately show ?thesis by auto |
|
302 qed |
|
303 qed |
|
304 qed |
|
305 |
|
306 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" |
|
307 by (rule ancenf_has_inum_aux[rule_format], auto) |
|
308 |
|
309 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'" |
|
310 by (auto dest:ancenf_has_inum) |
|
311 |
|
312 lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
313 by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum') |
|
314 |
|
315 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" |
|
316 by (drule file_leveling[rule_format], blast) |
|
317 |
|
318 lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
319 by (simp add:current_files_def, erule exE, auto intro:file_has_no_son) |
|
320 |
|
321 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" |
|
322 by (drule file_leveling[rule_format], blast) |
|
323 |
|
324 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" |
|
325 by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son) |
|
326 |
|
327 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" |
|
328 proof (induct f') |
|
329 case Nil |
|
330 show ?case |
|
331 by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits) |
|
332 next |
|
333 case (Cons a pf) |
|
334 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" |
|
335 show ?case |
|
336 proof clarify |
|
337 fix f |
|
338 assume h1: "f \<in> files_hung_by_del \<tau>" |
|
339 and h2: "valid \<tau>" |
|
340 and h3: "a # pf \<in> current_files \<tau>" |
|
341 and h4: "f \<preceq> a # pf" |
|
342 and h5: "f \<noteq> a # pf" |
|
343 have h6: "parent (a # pf) = Some pf" by simp |
|
344 with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
345 from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
346 show False |
|
347 proof (cases "f = pf") |
|
348 case True with h6 h2 h3 h1 |
|
349 show False by (auto intro!:hung_file_no_son') |
|
350 next |
|
351 case False with pre h1 h2 h7 h8 |
|
352 show False by blast |
|
353 qed |
|
354 qed |
|
355 qed |
|
356 |
|
357 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" |
|
358 by (rule hung_file_no_des_aux[rule_format], blast) |
|
359 |
|
360 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" |
|
361 apply (frule hung_file_has_inum', simp, erule exE) |
|
362 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) |
|
363 by (simp add: noJ_Anc, auto dest:hung_file_no_des) |
|
364 |
|
365 |
|
366 |
|
367 (************** file_of_proc_fd in current ********************) |
|
368 |
|
369 lemma file_of_pfd_imp_inode_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
370 apply (induct \<tau>) |
|
371 apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum) |
|
372 apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a) |
|
373 apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def |
|
374 split:if_splits option.splits) |
|
375 apply (simp add:pfdof_simp3)+ |
|
376 apply (simp add:proc_fd_of_file_def)+ |
|
377 done |
|
378 |
|
379 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" |
|
380 by (rule file_of_pfd_imp_inode_aux[rule_format], blast) |
|
381 |
|
382 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" |
|
383 by (auto dest!:file_of_pfd_imp_inode') |
|
384 |
|
385 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>" |
|
386 by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def) |
|
387 |
|
388 |
|
389 (*************** file_of_proc_fd is file *********************) |
|
390 |
|
391 lemma file_of_pfd_is_file_tag: |
|
392 "\<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" |
|
393 apply (induct \<tau> arbitrary:p, simp) |
|
394 apply (drule init_filefd_prop5, simp add:is_init_file_def split:option.splits t_inode_tag.splits) |
|
395 apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) |
|
396 by (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits |
|
397 dest:file_of_pfd_imp_inode' iof's_im_in_cim |
|
398 simp:is_file_def is_dir_def dir_is_empty_def current_files_def) |
|
399 |
|
400 lemma file_of_pfd_is_file: |
|
401 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
|
402 apply (frule file_of_pfd_imp_inode, simp, erule exE) |
|
403 apply (drule file_of_pfd_is_file_tag, simp+) |
|
404 by (simp add:is_file_def) |
|
405 |
|
406 lemma file_of_pfd_is_file': |
|
407 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
408 by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
409 |
|
410 (************** parent file / ancestral file is dir *******************) |
|
411 |
|
412 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" |
|
413 apply (induct \<tau>) |
|
414 apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir') |
|
415 apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a) |
|
416 apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps |
|
417 current_files_def is_dir_def is_file_def |
|
418 dest: ios's_im_in_cim iof's_im_in_cim |
|
419 split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits) |
|
420 apply (drule parentf_has_inum', simp, simp, simp)+ |
|
421 done |
|
422 |
|
423 lemma parentf_has_dirtag: |
|
424 "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk> |
|
425 \<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR" |
|
426 by (auto intro:parentf_is_dir_aux[rule_format]) |
|
427 |
|
428 lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
429 apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits) |
|
430 by (auto dest:parentf_has_dirtag) |
|
431 |
|
432 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf" |
|
433 by (clarsimp simp:current_files_def parentf_is_dir') |
|
434 |
|
435 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" |
|
436 proof (induct f') |
|
437 case Nil show ?case |
|
438 by (auto simp:current_files_def no_junior_def) |
|
439 next |
|
440 case (Cons a pf) |
|
441 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" |
|
442 show ?case |
|
443 proof clarify |
|
444 fix f |
|
445 assume h1: "f \<preceq> a # pf" |
|
446 and h2: "f \<noteq> a # pf" |
|
447 and h3: "a # pf \<in> current_files \<tau>" |
|
448 and h4: "valid \<tau>" |
|
449 have h5: "parent (a # pf) = Some pf" by simp |
|
450 with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto) |
|
451 from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def) |
|
452 show "is_dir \<tau> f" |
|
453 proof (cases "f = pf") |
|
454 case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto) |
|
455 next |
|
456 case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast |
|
457 qed |
|
458 qed |
|
459 qed |
|
460 |
|
461 lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f" |
|
462 by (auto intro:ancenf_is_dir_aux[rule_format]) |
|
463 |
|
464 (************* rebuild current_files simpset ***********************) |
|
465 |
|
466 lemma current_files_nil: "current_files [] = init_files" |
|
467 apply (simp add:current_files_def inum_of_file.simps) |
|
468 by (auto dest:inof_has_file_tag init_file_has_inum) |
|
469 |
|
470 lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)" |
|
471 by (auto simp add:current_files_def inum_of_file.simps split:option.splits) |
|
472 |
|
473 lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>" |
|
474 by (simp add:current_files_def inum_of_file.simps split:option.splits) |
|
475 |
|
476 lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = ( |
|
477 case (file_of_proc_fd \<tau> p fd) of |
|
478 Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>)) |
|
479 then current_files \<tau> - {f} |
|
480 else current_files \<tau>) |
|
481 | _ \<Rightarrow> current_files \<tau> )" |
|
482 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
483 |
|
484 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>)" |
|
485 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
486 |
|
487 lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then current_files \<tau> - {f} else current_files \<tau>)" |
|
488 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
489 |
|
490 lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)" |
|
491 by (auto simp:current_files_def inum_of_file.simps split:option.splits) |
|
492 |
|
493 lemma current_files_linkhard: |
|
494 "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>)" |
|
495 apply (frule vt_grant_os, frule vd_cons) |
|
496 by (auto simp:current_files_def inum_of_file.simps os_grant.simps split:option.splits) |
|
497 |
|
498 (* |
|
499 lemma rename_renaming_decom: |
|
500 "\<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" |
|
501 apply (case_tac "f\<^isub>2 \<preceq> f", simp) |
|
502 apply (simp add:file_after_rename_def split:if_splits) |
|
503 by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current) |
|
504 |
|
505 lemma rename_renaming_decom': |
|
506 "\<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" |
|
507 by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+) |
|
508 |
|
509 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>}" |
|
510 apply (frule vt_grant_os, frule vd_cons) |
|
511 apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits) |
|
512 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
513 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') |
|
514 apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp) |
|
515 apply (rule_tac x = x in exI, simp add:file_after_rename_def) |
|
516 apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp) |
|
517 apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp) |
|
518 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5) |
|
519 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
520 apply (simp add:file_after_rename_def) |
|
521 apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def) |
|
522 apply (simp add:file_after_rename_def) |
|
523 done |
|
524 *) |
|
525 |
|
526 lemma current_files_other: |
|
527 "\<lbrakk>\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
528 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
529 \<forall> p f. e \<noteq> UnLink p f; |
|
530 \<forall> p f. e \<noteq> Rmdir p f; |
|
531 \<forall> p f i. e \<noteq> Mkdir p f i; |
|
532 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>" |
|
533 by (case_tac e, auto simp:current_files_def inum_of_file.simps) |
|
534 |
|
535 lemmas current_files_simps = current_files_nil current_files_open current_files_open' |
|
536 current_files_closefd current_files_unlink current_files_rmdir |
|
537 current_files_mkdir current_files_linkhard current_files_other |
|
538 |
|
539 |
|
540 (******************** is_file simpset *********************) |
|
541 |
|
542 lemma is_file_nil: "is_file [] = is_init_file" |
|
543 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
|
544 |
|
545 lemma is_file_open: |
|
546 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
|
547 is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))" |
|
548 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
549 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
550 split:if_splits option.splits t_inode_tag.splits |
|
551 simp:is_file_def current_files_def) |
|
552 done |
|
553 |
|
554 lemma is_file_closefd: |
|
555 "valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = ( |
|
556 case (file_of_proc_fd s p fd) of |
|
557 Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s)) |
|
558 then (is_file s) (f := False) |
|
559 else is_file s) |
|
560 | _ \<Rightarrow> is_file s )" |
|
561 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
562 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
563 split:if_splits option.splits t_inode_tag.splits |
|
564 simp:is_file_def) |
|
565 done |
|
566 |
|
567 lemma is_file_unlink: |
|
568 "valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = ( |
|
569 if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)" |
|
570 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
571 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
572 split:if_splits option.splits t_inode_tag.splits |
|
573 simp:is_file_def) |
|
574 done |
|
575 |
|
576 lemma is_file_linkhard: |
|
577 "valid (LinkHard p f f' # s) \<Longrightarrow> is_file (LinkHard p f f' # s) = (is_file s) (f' := True)" |
|
578 apply (frule vd_cons, drule vt_grant_os, rule ext) |
|
579 apply (auto dest:finum_has_itag iof's_im_in_cim |
|
580 split:if_splits option.splits t_inode_tag.splits |
|
581 simp:is_file_def) |
|
582 done |
|
583 |
|
584 lemma is_file_other: |
|
585 "\<lbrakk>valid (e # \<tau>); |
|
586 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
587 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
588 \<forall> p f. e \<noteq> UnLink p f; |
|
589 \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> is_file (e # \<tau>) = is_file \<tau>" |
|
590 apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e) |
|
591 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
592 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
593 simp:is_file_def dir_is_empty_def is_dir_def current_files_def) |
|
594 done |
|
595 |
|
596 lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False" |
|
597 by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
598 |
|
599 lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f" |
|
600 by (rule notI, erule file_dir_conflict, simp) |
|
601 |
|
602 lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f" |
|
603 by (rule notI, erule file_dir_conflict, simp) |
|
604 |
|
605 lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other |
|
606 |
|
607 (********* is_dir simpset **********) |
|
608 |
|
609 lemma is_dir_nil: "is_dir [] = is_init_dir" |
|
610 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) |
|
611 |
|
612 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)" |
|
613 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
614 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
615 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
616 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
617 done |
|
618 |
|
619 lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)" |
|
620 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
|
621 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
|
622 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
|
623 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
|
624 apply (drule pfdof_simp2) |
|
625 apply (drule file_of_pfd_is_file, simp) |
|
626 apply (simp add:is_file_def split:t_inode_tag.splits option.splits) |
|
627 done |
|
628 |
|
629 lemma is_dir_other: |
|
630 "\<lbrakk>valid (e # s); |
|
631 \<forall> p f. e \<noteq> Rmdir p f; |
|
632 \<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s" |
|
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 apply (drule file_of_pfd_is_file, simp) |
|
638 apply (simp add:is_file_def split:t_inode_tag.splits option.splits) |
|
639 done |
|
640 |
|
641 lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other |
|
642 |
|
643 (*********** no root dir involved ***********) |
|
644 |
|
645 lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []" |
|
646 apply (induct s, simp add:is_dir_nil root_is_init_dir) |
|
647 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
648 apply (auto simp:is_dir_simps) |
|
649 done |
|
650 |
|
651 lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False" |
|
652 apply (drule root_is_dir) |
|
653 apply (erule file_dir_conflict, simp) |
|
654 done |
|
655 |
|
656 lemma noroot_execve: |
|
657 "valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []" |
|
658 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
659 |
|
660 lemma noroot_execve': |
|
661 "valid (Execve p [] fds # s) \<Longrightarrow> False" |
|
662 by (drule noroot_execve, simp) |
|
663 |
|
664 lemma noroot_open: |
|
665 "valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []" |
|
666 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits) |
|
667 |
|
668 lemma noroot_open': |
|
669 "valid (Open p [] flags fd opt # s) \<Longrightarrow> False" |
|
670 by (drule noroot_open, simp) |
|
671 |
|
672 lemma noroot_filefd': |
|
673 "\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False" |
|
674 apply (induct s arbitrary:p, simp) |
|
675 apply (drule init_filefd_prop5, erule root_is_init_dir') |
|
676 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
677 apply (auto split:if_splits option.splits dest!:root_is_dir') |
|
678 done |
|
679 |
|
680 lemma noroot_filefd: |
|
681 "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []" |
|
682 by (rule notI, simp, erule noroot_filefd', simp) |
|
683 |
|
684 lemma noroot_unlink: |
|
685 "valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []" |
|
686 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
687 |
|
688 lemma noroot_unlink': |
|
689 "valid (UnLink p [] # s) \<Longrightarrow> False" |
|
690 by (drule noroot_unlink, simp) |
|
691 |
|
692 lemma noroot_rmdir: |
|
693 "valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []" |
|
694 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
695 |
|
696 lemma noroot_rmdir': |
|
697 "valid (Rmdir p [] # s) \<Longrightarrow> False" |
|
698 by (drule noroot_rmdir, simp) |
|
699 |
|
700 lemma noroot_mkdir: |
|
701 "valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []" |
|
702 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
703 |
|
704 lemma noroot_mkdir': |
|
705 "valid (Mkdir p [] inum # s) \<Longrightarrow> False" |
|
706 by (drule noroot_mkdir, simp) |
|
707 |
|
708 lemma noroot_linkhard: |
|
709 "valid (LinkHard p f f' # s) \<Longrightarrow> f \<noteq> [] \<and> f' \<noteq> []" |
|
710 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
711 |
|
712 lemma noroot_linkhard': |
|
713 "valid (LinkHard p [] f # s) \<Longrightarrow> False" |
|
714 by (drule noroot_linkhard, simp) |
|
715 |
|
716 lemma noroot_linkhard'': |
|
717 "valid (LinkHard p f [] # s) \<Longrightarrow> False" |
|
718 by (drule noroot_linkhard, simp) |
|
719 |
|
720 lemma noroot_truncate: |
|
721 "valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []" |
|
722 by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir') |
|
723 |
|
724 lemma noroot_truncate': |
|
725 "valid (Truncate p [] len # s) \<Longrightarrow> False" |
|
726 by (drule noroot_truncate, simp) |
|
727 |
|
728 lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir |
|
729 noroot_mkdir noroot_linkhard noroot_truncate |
|
730 |
|
731 lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir' |
|
732 noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate' |
|
733 |
|
734 end |
|
735 |
|
736 end |