130 apply (frule cf2sfile_path_file, simp) defer |
130 apply (frule cf2sfile_path_file, simp) defer |
131 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file) |
131 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file) |
132 apply (auto split:option.splits) |
132 apply (auto split:option.splits) |
133 done |
133 done |
134 |
134 |
135 |
135 lemma cf2sfile_path_file_prop1: |
136 |
136 "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk> |
137 apply simp |
137 \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = |
138 |
138 Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
139 thm cf2sfile_def |
139 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> |
140 apply (simp (no_asm_simp)) |
140 sectxt_of_obj s (O_file (f # pf)) = Some fsec" |
141 apply simp |
141 apply (frule is_file_has_sfile, simp) |
142 apply (frule cf2sfile_path_file, simp) |
142 by (auto simp:cf2sfile_path_file) |
143 apply (simp add: cf2sfile_path_file) |
143 |
144 apply auto |
144 lemma cf2sfile_path_file_prop2: |
145 apply (simp only:cf2sfile_path_file) |
145 "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); |
146 by (simp add:cf2sfile_path_file cf2sfile_path_dir) |
146 sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = |
147 apply (frule parentf_is_dir'', simp) |
147 Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf) |
148 apply (frule is_file_or_dir, simp) |
148 else Created, fsec, Some pfsec, asecs \<union> {pfsec})" |
149 apply (frule sroot_set, erule disjE) |
149 by (drule cf2sfile_path_file_prop1, auto) |
150 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp) |
150 |
151 apply (case_tac pf, clarsimp) |
151 lemma cf2sfile_path_dir_prop1: |
152 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps |
152 "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk> |
153 simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] |
153 \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = |
154 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop |
154 Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf) |
155 simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] |
155 else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> |
156 apply (case_tac "is_file s (f # pf)") |
156 sectxt_of_obj s (O_dir (f # pf)) = Some fsec" |
157 apply (frule is_file_has_sec, simp) |
157 apply (frule is_dir_has_sfile, simp) |
158 apply (frule is_dir_has_sec, simp) |
158 by (auto simp:cf2sfile_path_dir) |
159 apply (frule is_dir_not_file) |
159 |
160 apply (erule exE)+ |
160 lemma cf2sfile_path_dir_prop2: |
161 apply (auto split:option.splits)[1] |
161 "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); |
162 apply simp |
162 sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = |
163 |
163 Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf) |
164 apply (rule ext) |
164 else Created, fsec, Some pfsec, asecs \<union> {pfsec})" |
165 apply (subst (1) cf2sfile_def) |
165 by (drule cf2sfile_path_dir_prop1, auto) |
166 apply (auto simp del:deleted.simps get_parentfs_ctxts.simps split:option.splits if_splits) |
166 |
167 |
167 (**************** cf2sfile event list simpset ****************) |
168 lemma cf2sfile_open_none1: |
168 |
169 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" |
169 lemma cf2sfile_open_none': |
170 apply (frule vd_cons, frule vt_grant_os) |
170 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'" |
171 apply (frule noroot_events, case_tac f, simp) |
|
172 apply (auto split:if_splits option.splits dest!:current_has_sec' dest:parentf_in_current' |
|
173 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
174 get_parentfs_ctxts_simps) |
|
175 done |
|
176 |
|
177 lemma cf2sfile_open_none2: |
|
178 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b" |
|
179 apply (frule vd_cons, frule vt_grant_os) |
171 apply (frule vd_cons, frule vt_grant_os) |
180 apply (induct f', simp add:cf2sfile_def) |
172 apply (induct f', simp add:cf2sfile_def) |
181 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
173 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
182 get_parentfs_ctxts_simps) |
174 get_parentfs_ctxts_simps) |
183 done |
175 done |
184 |
176 |
185 lemma cf2sfile_open_none: |
177 lemma cf2sfile_open_none: |
186 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s" |
178 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s" |
187 apply (rule ext, rule ext) |
179 apply (rule ext) |
188 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2) |
180 by (simp add:cf2sfile_open_none') |
189 done |
|
190 |
181 |
191 lemma cf2sfile_open_some1: |
182 lemma cf2sfile_open_some1: |
192 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
183 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
193 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
184 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
194 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
185 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
195 apply (case_tac "f = f'", simp) |
186 apply (case_tac "f = f'", simp) |
196 apply (induct f', simp add:sroot_only, simp) |
187 apply (induct f', simp add:sroot_only, simp) |
197 apply (frule parentf_in_current', simp+) |
188 apply (frule parentf_in_current', simp+) |
198 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
189 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
199 get_parentfs_ctxts_simps) |
190 get_parentfs_ctxts_simps) |
200 done |
191 done |
201 |
192 |
202 lemma cf2sfile_open_some2: |
193 lemma cf2sfile_open_some2: |
203 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
194 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
204 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True" |
195 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
205 apply (frule vd_cons, drule is_file_in_current) |
196 apply (frule vd_cons, drule is_file_in_current) |
206 by (simp add:cf2sfile_open_some1) |
197 by (simp add:cf2sfile_open_some1) |
207 |
198 |
208 lemma cf2sfile_open_some3: |
199 lemma cf2sfile_open_some3: |
209 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
200 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
210 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False" |
201 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
211 apply (frule vd_cons, drule is_dir_in_current) |
202 apply (frule vd_cons, drule is_dir_in_current) |
212 by (simp add:cf2sfile_open_some1) |
203 by (simp add:cf2sfile_open_some1) |
213 |
204 |
214 lemma cf2sfile_open_some4: |
205 lemma cf2sfile_open_some4: |
215 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = ( |
206 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = ( |
216 case (parent f) of |
207 case (parent f) of |
217 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), |
208 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), |
218 get_parentfs_ctxts s pf) of |
209 get_parentfs_ctxts s pf) of |
219 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
210 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
220 | _ \<Rightarrow> None) |
211 | _ \<Rightarrow> None) |
226 apply (rule impI, (erule conjE)+) |
217 apply (rule impI, (erule conjE)+) |
227 apply (drule not_deleted_init_file, simp+) |
218 apply (drule not_deleted_init_file, simp+) |
228 apply (simp add:is_file_in_current) |
219 apply (simp add:is_file_in_current) |
229 done |
220 done |
230 |
221 |
231 lemma cf2sfile_open_some5: |
|
232 "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> |
|
233 cf2sfile (Open p f flag fd (Some inum) # s) f False = cf2sfile s f False" |
|
234 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
235 apply (case_tac f, simp) |
|
236 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
237 get_parentfs_ctxts_simps split:option.splits) |
|
238 done |
|
239 |
|
240 lemma cf2sfile_open: |
222 lemma cf2sfile_open: |
241 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
223 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
242 \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' b = ( |
224 \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = ( |
243 if (opt = None) then cf2sfile s f' b |
225 if (opt = None) then cf2sfile s f' |
244 else if (f' = f \<and> b) |
226 else if (f' = f) |
245 then (case (parent f) of |
227 then (case (parent f) of |
246 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), |
228 Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), |
247 get_parentfs_ctxts s pf) of |
229 get_parentfs_ctxts s pf) of |
248 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
230 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
249 | _ \<Rightarrow> None) |
231 | _ \<Rightarrow> None) |
250 | None \<Rightarrow> None) |
232 | None \<Rightarrow> None) |
251 else cf2sfile s f' b)" |
233 else cf2sfile s f')" |
252 apply (case_tac opt) |
234 apply (case_tac opt) |
253 apply (simp add:cf2sfile_open_none) |
235 apply (simp add:cf2sfile_open_none) |
254 apply (case_tac "f = f'") |
236 apply (case_tac "f = f'") |
255 apply (auto simp:cf2sfile_open_some1 cf2sfile_open_some4 cf2sfile_open_some5 current_files_simps) |
237 apply (simp add:cf2sfile_open_some4 split:option.splits) |
|
238 apply (simp add:cf2sfile_open_some1 current_files_simps) |
256 done |
239 done |
257 |
240 |
258 lemma cf2sfile_mkdir1: |
241 lemma cf2sfile_mkdir1: |
259 "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk> |
242 "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk> |
260 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'" |
243 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'" |
261 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
244 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
262 apply (case_tac "f = f'", simp) |
245 apply (case_tac "f = f'", simp) |
263 apply (induct f', simp add:sroot_only, simp) |
246 apply (induct f', simp add:sroot_only, simp) |
264 apply (frule parentf_in_current', simp+) |
247 apply (frule parentf_in_current', simp+) |
265 apply clarsimp |
248 apply (case_tac "f = f'", simp) |
266 apply (case_tac "f = f'", simp+) |
249 apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
267 apply (simp (no_asm_simp) add:cf2sfile_def) |
250 get_parentfs_ctxts_simps split:if_splits option.splits) |
|
251 done |
|
252 |
|
253 lemma cf2sfile_mkdir2: |
|
254 "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk> |
|
255 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'" |
|
256 apply (frule vd_cons, drule is_file_in_current) |
|
257 by (simp add:cf2sfile_mkdir1) |
|
258 |
|
259 lemma cf2sfile_mkdir3: |
|
260 "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk> |
|
261 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'" |
|
262 apply (frule vd_cons, drule is_dir_in_current) |
|
263 by (simp add:cf2sfile_mkdir1) |
|
264 |
|
265 lemma cf2sfile_mkdir4: |
|
266 "valid (Mkdir p f i # s) |
|
267 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of |
|
268 Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), |
|
269 get_parentfs_ctxts s pf) of |
|
270 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
|
271 | _ \<Rightarrow> None) |
|
272 | None \<Rightarrow> None)" |
|
273 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
274 apply (case_tac f, simp) |
|
275 apply (clarsimp simp:os_grant.simps) |
|
276 apply (simp add:sectxt_of_obj_simps) |
|
277 apply (frule current_proc_has_sec, simp) |
|
278 apply (frule is_dir_has_sec, simp) |
|
279 apply (frule get_pfs_secs_prop, simp) |
|
280 apply (frule is_dir_not_file) |
268 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
281 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
269 get_parentfs_ctxts_simps split:if_splits option.splits) |
282 get_parentfs_ctxts_simps split:option.splits if_splits |
270 done |
283 dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current) |
271 |
284 done |
272 lemma cf2sfile_mkdir2: |
|
273 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
|
274 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True" |
|
275 apply (frule vd_cons, drule is_file_in_current) |
|
276 by (simp add:cf2sfile_open_some1) |
|
277 |
|
278 lemma cf2sfile_mkdir3: |
|
279 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk> |
|
280 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False" |
|
281 apply (frule vd_cons, drule is_dir_in_current) |
|
282 by (simp add:cf2sfile_open_some1) |
|
283 |
|
284 |
285 |
285 lemma cf2sfile_mkdir: |
286 lemma cf2sfile_mkdir: |
286 "valid (Mkdir p f i # s) |
287 "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk> |
287 \<Longrightarrow> cf2sfile (Mkdir p f i # s) = (\<lambda> f' b. |
288 \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = ( |
288 if (f' = f \<and> \<not> b) |
289 if (f' = f) |
289 then (case (parent f) of |
290 then (case (parent f) of |
290 Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), |
291 Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), |
291 get_parentfs_ctxts s pf) of |
292 get_parentfs_ctxts s pf) of |
292 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
293 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
293 | _ \<Rightarrow> None) |
294 | _ \<Rightarrow> None) |
294 | None \<Rightarrow> None) |
295 | None \<Rightarrow> None) |
295 else cf2sfile s f' b)" |
296 else cf2sfile s f')" |
|
297 apply (case_tac "f = f'") |
|
298 apply (simp add:cf2sfile_mkdir4 split:option.splits) |
|
299 apply (simp add:cf2sfile_mkdir1 current_files_simps) |
|
300 done |
|
301 |
|
302 lemma cf2sfile_linkhard1: |
|
303 "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk> |
|
304 \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'" |
|
305 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
306 apply (case_tac "f = f'", simp) |
|
307 apply (induct f', simp add:sroot_only, simp) |
|
308 apply (frule parentf_in_current', simp+) |
|
309 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
310 get_parentfs_ctxts_simps split:if_splits option.splits) |
|
311 done |
|
312 |
|
313 lemma cf2sfile_linkhard2: |
|
314 "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk> |
|
315 \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'" |
|
316 apply (frule vd_cons, drule is_file_in_current) |
|
317 by (simp add:cf2sfile_linkhard1) |
|
318 |
|
319 lemma cf2sfile_linkhard3: |
|
320 "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk> |
|
321 \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'" |
|
322 apply (frule vd_cons, drule is_dir_in_current) |
|
323 by (simp add:cf2sfile_linkhard1) |
|
324 |
|
325 lemma cf2sfile_linkhard4: |
|
326 "valid (LinkHard p oldf f # s) |
|
327 \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of |
|
328 Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), |
|
329 get_parentfs_ctxts s pf) of |
|
330 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
|
331 | _ \<Rightarrow> None) |
|
332 | None \<Rightarrow> None)" |
|
333 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
334 apply (case_tac f, simp) |
|
335 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
336 get_parentfs_ctxts_simps) |
|
337 apply (rule impI, (erule conjE)+) |
|
338 apply (drule not_deleted_init_file, simp+) |
|
339 apply (simp add:is_file_in_current) |
|
340 done |
|
341 |
|
342 lemma cf2sfile_linkhard: |
|
343 "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk> |
|
344 \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = ( |
|
345 if (f' = f) |
|
346 then (case (parent f) of |
|
347 Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), |
|
348 get_parentfs_ctxts s pf) of |
|
349 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
|
350 | _ \<Rightarrow> None) |
|
351 | None \<Rightarrow> None) |
|
352 else cf2sfile s f')" |
|
353 apply (case_tac "f = f'") |
|
354 apply (simp add:cf2sfile_linkhard4 split:option.splits) |
|
355 apply (simp add:cf2sfile_linkhard1 current_files_simps) |
|
356 done |
|
357 |
|
358 lemma cf2sfile_other: |
|
359 "\<lbrakk>ff \<in> current_files s; |
|
360 \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt; |
|
361 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
362 \<forall> p f. e \<noteq> UnLink p f; |
|
363 \<forall> p f. e \<noteq> Rmdir p f; |
|
364 \<forall> p f i. e \<noteq> Mkdir p f i; |
|
365 \<forall> p f f'. e \<noteq> LinkHard p f f'; |
|
366 valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff" |
296 apply (frule vd_cons, frule vt_grant_os) |
367 apply (frule vd_cons, frule vt_grant_os) |
297 apply (rule ext, rule ext) |
368 apply (induct ff, simp add:sroot_only) |
298 |
369 apply (frule parentf_in_current', simp+, case_tac e) |
299 apply (auto simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
370 apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path |
300 get_parentfs_ctxts_simps split:if_splits option.splits) |
371 split:if_splits option.splits) |
301 |
372 done |
302 |
373 |
303 |
374 lemma cf2sfile_unlink: |
304 |
375 "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> |
|
376 \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'" |
|
377 apply (frule vd_cons, frule vt_grant_os) |
|
378 apply (simp add:current_files_simps split:if_splits) |
|
379 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps |
|
380 split:if_splits option.splits) |
|
381 |
|
382 |
|
383 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other |
|
384 |
305 |
385 |
306 |
386 |
307 |
387 |
308 |
388 |
309 |
389 |