|
1 theory Proc_fd_of_file_prop |
|
2 imports Main Flask Flask_type Valid_prop Current_files_prop |
|
3 begin |
|
4 |
|
5 context flask begin |
|
6 |
|
7 lemma proc_fd_in_procs: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>" |
|
8 apply (induct \<tau> arbitrary: f) defer |
|
9 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
10 apply (auto simp:file_of_proc_fd.simps current_procs.simps os_grant.simps split:if_splits option.splits) |
|
11 by (drule init_filefd_valid, simp) |
|
12 |
|
13 lemma proc_fd_in_fds_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p" |
|
14 apply (induct \<tau>) |
|
15 apply (simp add:file_of_proc_fd.simps current_proc_fds.simps) |
|
16 apply (clarify, drule init_filefd_valid, simp) |
|
17 apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a) |
|
18 apply (auto simp:file_of_proc_fd.simps current_proc_fds.simps split:if_splits option.splits t_sock_addr.splits) |
|
19 done |
|
20 |
|
21 lemma proc_fd_in_fds: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p" |
|
22 by (rule proc_fd_in_fds_aux[rule_format], simp+) |
|
23 |
|
24 lemma proc_fd_file_in_cur: "\<lbrakk>(p, fd) \<in> proc_fd_of_file \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
25 by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current) |
|
26 |
|
27 lemma proc_fd_file_in_cur': "\<lbrakk>proc_fd_of_file \<tau> f \<noteq> {}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
28 by (auto simp:proc_fd_file_in_cur) |
|
29 |
|
30 lemma proc_fd_file_in_cur'': "\<lbrakk>proc_fd_of_file \<tau> f = {(p,fd)}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
31 by (auto simp:proc_fd_file_in_cur') |
|
32 |
|
33 lemma procfd_of_file_imp_fpfd: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f" |
|
34 by (auto simp:proc_fd_of_file_def) |
|
35 |
|
36 lemma procfd_of_file_imp_fpfd': "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd \<noteq> None" |
|
37 by (auto simp:proc_fd_of_file_def) |
|
38 |
|
39 lemma procfd_of_file_eq_fpfd'': "(p, fd) \<in> proc_fd_of_file \<tau> f = (file_of_proc_fd \<tau> p fd = Some f)" |
|
40 by (auto simp:proc_fd_of_file_def) |
|
41 |
|
42 lemma procfd_of_file_non_empty: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> proc_fd_of_file \<tau> f \<noteq> {}" |
|
43 by (auto simp:proc_fd_of_file_def) |
|
44 |
|
45 lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>" |
|
46 by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur') |
|
47 |
|
48 |
|
49 (******************* rebuild proc_fd_of_file simpset ***********************) |
|
50 (* |
|
51 lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> |
|
52 proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')" |
|
53 apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits) |
|
54 apply (frule vd_cons, drule vt_grant_os, case_tac iopt) |
|
55 apply (drule proc_fd_in_fds, simp, simp add:os_grant.simps nfd_notin_curfd)+ |
|
56 done |
|
57 |
|
58 lemma proc_fd_of_file_closefd: "proc_fd_of_file (CloseFd p fd # \<tau>) f = (if (file_of_proc_fd \<tau> p fd = Some f) then (proc_fd_of_file \<tau> f - {(p,fd)}) else proc_fd_of_file \<tau> f) " |
|
59 by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits) |
|
60 |
|
61 lemma proc_fd_of_file_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow> |
|
62 proc_fd_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (if (f\<^isub>3 \<preceq> f) then proc_fd_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else proc_fd_of_file \<tau> f)" |
|
63 apply (frule vt_grant_os, frule vd_cons) |
|
64 apply (case_tac "f\<^isub>3 \<preceq> f") |
|
65 apply (subgoal_tac "f \<notin> current_files \<tau>") prefer 2 apply (rule notI) |
|
66 apply (clarsimp simp:os_grant.simps, drule_tac f = f\<^isub>3 and f' = f in ancenf_in_current, simp, simp, simp) |
|
67 apply (auto simp add:proc_fd_of_file_def)[1] |
|
68 |
|
69 apply (simp add:file_of_proc_fd.simps split:option.splits if_splits) |
|
70 apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = aa and f\<^isub>2 = f\<^isub>2 in file_renaming_prop5, simp) |
|
71 apply (drule file_of_pfd_in_current, simp+) |
|
72 apply (simp add:file_of_proc_fd.simps) |
|
73 apply (rule conjI, rule impI, simp add:file_renaming_prop5') |
|
74 apply (rule impI, simp add:file_before_rename_def) |
|
75 |
|
76 apply (simp add:proc_fd_of_file_def split:if_splits) |
|
77 apply auto |
|
78 apply (simp add:file_of_proc_fd.simps split:option.splits if_splits) |
|
79 apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>2 = f\<^isub>2 and f = aa in file_renaming_prop1, simp) |
|
80 apply (simp add:current_files_simps) |
|
81 apply (erule exE| erule conjE)+ |
|
82 apply (simp add:file_of_proc_fd.simps split:option.splits if_splits) |
|
83 apply (drule_tac f = f\<^isub>1 in rename_renaming_decom', simp+) |
|
84 apply (simp add:file_after_rename_def) |
|
85 done |
|
86 |
|
87 |
|
88 lemma proc_fd_of_file_kill: "proc_fd_of_file (Kill p\<^isub>1 p\<^isub>2 # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p\<^isub>2}" |
|
89 by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps) |
|
90 |
|
91 lemma proc_fd_of_file_exit: "proc_fd_of_file (Exit p' # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p'}" |
|
92 by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps) |
|
93 |
|
94 lemma proc_fd_of_file_clone: "Clone p\<^isub>1 p\<^isub>2 # valid \<tau> \<Longrightarrow> proc_fd_of_file (Clone p\<^isub>1 p\<^isub>2 # \<tau>) f = proc_fd_of_file \<tau> f \<union> {(p\<^isub>2, fd)| fd. (p\<^isub>1, fd) \<in> proc_fd_of_file \<tau> f}" |
|
95 apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps) |
|
96 apply (frule vd_cons, drule vt_grant_os) |
|
97 apply (drule proc_fd_in_procs, (simp add:os_grant.simps np_notin_curp)+) |
|
98 done |
|
99 |
|
100 lemma proc_fd_of_file_other: "\<lbrakk>e # valid \<tau>; |
|
101 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
102 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
103 \<forall> p f f'. e \<noteq> Rename p f f'; |
|
104 \<forall> p p'. e \<noteq> Kill p p'; |
|
105 \<forall> p. e \<noteq> Exit p; |
|
106 \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> proc_fd_of_file (e # \<tau>) f = proc_fd_of_file \<tau> f" |
|
107 apply (case_tac e, auto simp:proc_fd_of_file_def file_of_proc_fd.simps) |
|
108 done |
|
109 |
|
110 lemmas proc_fd_of_file_simps = proc_fd_of_file_open proc_fd_of_file_closefd proc_fd_of_file_rename proc_fd_of_file_kill proc_fd_of_file_exit proc_fd_of_file_clone proc_fd_of_file_other |
|
111 *) |
|
112 end |
|
113 |
|
114 |
|
115 end |