8 |
8 |
9 (************ simpset for cf2sfile ***************) |
9 (************ simpset for cf2sfile ***************) |
10 |
10 |
11 declare get_parentfs_ctxts.simps [simp del] |
11 declare get_parentfs_ctxts.simps [simp del] |
12 |
12 |
13 lemma cf2sfile_open_none: |
13 lemma cf2sfile_open_none1: |
14 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" |
14 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b" |
15 apply (frule vd_cons, frule vt_grant_os) |
15 apply (frule vd_cons, frule vt_grant_os) |
16 apply (frule noroot_events) |
16 apply (frule noroot_events, case_tac f, simp) |
17 by (auto split:if_splits option.splits dest!:current_has_sec' |
17 apply (auto split:if_splits option.splits dest!:current_has_sec' dest:parentf_in_current' |
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 done |
|
21 |
|
22 lemma cf2sfile_open_none2: |
|
23 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b" |
|
24 apply (frule vd_cons, frule vt_grant_os) |
|
25 apply (induct f', simp add:cf2sfile_def) |
|
26 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
27 get_parentfs_ctxts_simps) |
|
28 done |
|
29 |
|
30 lemma cf2sfile_open_none: |
|
31 "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s" |
|
32 apply (rule ext, rule ext) |
|
33 apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2) |
|
34 done |
20 |
35 |
21 lemma sroot_only: |
36 lemma sroot_only: |
22 "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)" |
37 "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)" |
23 by (rule ext, simp add:cf2sfile_def) |
38 by (rule ext, simp add:cf2sfile_def) |
24 |
39 |
25 lemma cf2sfile_open_some1: |
40 lemma cf2sfile_open_some1: |
26 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
41 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk> |
27 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
42 \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'" |
28 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
43 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext) |
29 apply (induct f', simp add:sroot_only) |
44 apply (case_tac "f = f'", simp) |
30 apply simp |
45 apply (induct f', simp add:sroot_only, simp) |
31 apply (frule parentf_in_current', simp+) |
46 apply (frule parentf_in_current', simp+) |
32 apply (auto simp:cf2sfile_def split:if_splits option.splits) |
47 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
33 apply (auto split:if_splits option.splits dest!:current_has_sec' |
|
34 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
35 get_parentfs_ctxts_simps) |
48 get_parentfs_ctxts_simps) |
36 done |
49 done |
37 |
50 |
38 lemma cf2sfile_open_some2: |
51 lemma cf2sfile_open_some2: |
39 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
52 "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk> |
54 get_parentfs_ctxts s pf) of |
67 get_parentfs_ctxts s pf) of |
55 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
68 (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs) |
56 | _ \<Rightarrow> None) |
69 | _ \<Rightarrow> None) |
57 | None \<Rightarrow> None)" |
70 | None \<Rightarrow> None)" |
58 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
71 apply (frule vd_cons, frule vt_grant_os, frule noroot_events) |
|
72 apply (case_tac f, simp) |
|
73 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
|
74 get_parentfs_ctxts_simps) |
|
75 apply (rule impI) |
|
76 thm not_deleted_imp_exists |
59 apply (auto split:if_splits option.splits dest!:current_has_sec' |
77 apply (auto split:if_splits option.splits dest!:current_has_sec' |
60 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
78 simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps |
61 get_parentfs_ctxts_simps) |
79 get_parentfs_ctxts_simps) |
62 |
80 |
63 |
81 |