16 apply (frule noroot_events) |
16 apply (frule noroot_events) |
17 by (auto split:if_splits option.splits dest!:current_has_sec' |
17 by (auto split:if_splits option.splits dest!:current_has_sec' |
18 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
18 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
19 get_parentfs_ctxts_simps) |
19 get_parentfs_ctxts_simps) |
20 |
20 |
|
21 lemma sroot_only: |
|
22 "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)" |
|
23 by (rule ext, simp add:cf2sfile_def) |
|
24 |
21 lemma cf2sfile_open_some1: |
25 lemma cf2sfile_open_some1: |
22 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
26 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
23 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
27 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
24 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
28 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
25 apply (induct f') |
29 apply (induct f', simp add:sroot_only) |
|
30 apply simp |
|
31 apply (frule parentf_in_current', simp+) |
|
32 apply (auto simp:cf2sfile_def split:if_splits option.splits) |
26 apply (auto split:if_splits option.splits dest!:current_has_sec' |
33 apply (auto split:if_splits option.splits dest!:current_has_sec' |
27 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
34 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
28 get_parentfs_ctxts_simps) |
35 get_parentfs_ctxts_simps) |
29 done |
36 done |
30 |
37 |