|
1 theory finite_static |
|
2 imports Main rc_theory all_sobj_prop |
|
3 begin |
|
4 |
|
5 context tainting_s_complete begin |
|
6 |
|
7 lemma tainted_s_subset_all_sobjs: |
|
8 "tainted_s \<subseteq> all_sobjs" |
|
9 apply (rule subsetI, erule tainted_s.induct) |
|
10 apply (auto intro:all_sobjs.intros) |
|
11 apply (drule seeds_in_init) |
|
12 apply (subgoal_tac "exists [] obj") |
|
13 apply (frule obj2sobj_nil_init) |
|
14 apply (drule all_sobjs_I) |
|
15 apply (rule vs_nil, simp) |
|
16 apply (case_tac obj, simp+) |
|
17 done |
|
18 |
|
19 definition |
|
20 "init_proc_opt \<equiv> {Some p | p. p \<in> init_processes} \<union> {None}" |
|
21 |
|
22 lemma finite_init_proc_opt: |
|
23 "finite init_proc_opt" |
|
24 unfolding init_proc_opt_def |
|
25 apply (simp add: finite_Un) |
|
26 apply (rule finite_imageI) |
|
27 by (simp add:init_finite) |
|
28 |
|
29 definition |
|
30 "init_file_opt \<equiv> {Some f | f. f \<in> init_files} \<union> {None}" |
|
31 |
|
32 lemma finite_init_file_opt: |
|
33 "finite init_file_opt" |
|
34 unfolding init_file_opt_def |
|
35 apply (simp add: finite_Un) |
|
36 apply (rule finite_imageI) |
|
37 by (simp add:init_finite) |
|
38 |
|
39 definition |
|
40 "init_ipc_opt \<equiv> {Some i | i. i \<in> init_processes} \<union> {None}" |
|
41 |
|
42 lemma finite_init_ipc_opt: |
|
43 "finite init_ipc_opt" |
|
44 unfolding init_ipc_opt_def |
|
45 apply (simp add: finite_Un) |
|
46 apply (rule finite_imageI) |
|
47 by (simp add:init_finite) |
|
48 |
|
49 lemma finite_t_client: |
|
50 "finite (UNIV :: t_client set)" |
|
51 apply (subgoal_tac "UNIV = {Client1, Client2}") |
|
52 apply (metis (full_types) finite.emptyI finite_insert) |
|
53 apply auto |
|
54 apply (case_tac x, simp+) |
|
55 done |
|
56 |
|
57 lemma finite_t_normal_role: |
|
58 "finite (UNIV :: t_normal_role set)" |
|
59 proof- |
|
60 have p1: "finite {WebServer}" by simp |
|
61 have p2: "finite {WS c | c. c \<in> UNIV}" using finite_t_client by auto |
|
62 have p3: "finite {UpLoad c| c. c \<in> UNIV}" using finite_t_client by auto |
|
63 have p4: "finite {CGI c| c. c \<in> UNIV}" using finite_t_client by auto |
|
64 from p1 p2 p3 p4 |
|
65 have p5: "finite ({WebServer} \<union> {WS c | c. c \<in> UNIV} \<union> {UpLoad c | c. c \<in> UNIV} \<union> {CGI c | c. c \<in> UNIV})" |
|
66 by auto |
|
67 have p6: "(UNIV :: t_normal_role set) = ({WebServer} \<union> {WS c | c. c \<in> UNIV} \<union> |
|
68 {UpLoad c | c. c \<in> UNIV} \<union> {CGI c | c. c \<in> UNIV})" |
|
69 apply (rule set_eqI, auto split:t_normal_role.splits) |
|
70 by (case_tac x, auto) |
|
71 show ?thesis by (simp only:p6 p5) |
|
72 qed |
|
73 |
|
74 lemma finite_t_role: "finite (UNIV :: t_role set)" |
|
75 proof- |
|
76 have p1: "finite {NormalRole r | r. r \<in> UNIV}" using finite_t_normal_role by auto |
|
77 have p2: "finite {InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole}" |
|
78 by auto |
|
79 have p3: "UNIV = {InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole} \<union> |
|
80 {NormalRole r | r. r \<in> UNIV}" |
|
81 apply (rule set_eqI, auto split:t_role.splits) |
|
82 by (case_tac x, auto) |
|
83 have p4: "finite ({InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole} \<union> |
|
84 {NormalRole r | r. r \<in> UNIV})" using p1 p2 by auto |
|
85 show ?thesis by (simp only:p3 p4) |
|
86 qed |
|
87 |
|
88 lemma finite_t_normal_file_type: "finite (UNIV :: t_normal_file_type set)" |
|
89 proof- |
|
90 have p1: "finite {WebData_file c | c. c \<in> UNIV}" using finite_t_client by auto |
|
91 have p2: "finite {CGI_P_file c | c. c \<in> UNIV}" using finite_t_client by auto |
|
92 have p3: "finite {PrivateD_file c | c. c \<in> UNIV}" using finite_t_client by auto |
|
93 have p4: "finite {Executable_file, Root_file_type, WebServerLog_file}" by auto |
|
94 have p5: "finite ({WebData_file c | c. c \<in> UNIV} \<union> {CGI_P_file c | c. c \<in> UNIV} \<union> |
|
95 {PrivateD_file c | c. c \<in> UNIV} \<union> {Executable_file, Root_file_type, WebServerLog_file})" |
|
96 using p1 p2 p3 p4 by auto |
|
97 have p6: "UNIV = ({WebData_file c | c. c \<in> UNIV} \<union> {CGI_P_file c | c. c \<in> UNIV} \<union> |
|
98 {PrivateD_file c | c. c \<in> UNIV} \<union> {Executable_file, Root_file_type, WebServerLog_file})" |
|
99 apply (rule set_eqI, auto split:t_normal_file_type.splits) |
|
100 by (case_tac x, auto) |
|
101 show ?thesis by (simp only:p6 p5) |
|
102 qed |
|
103 |
|
104 lemma finite_t_rc_file_type: "finite (UNIV :: t_rc_file_type set)" |
|
105 proof- |
|
106 have p1: "finite {NormalFile_type t | t. t \<in> UNIV}" using finite_t_normal_file_type by auto |
|
107 have p2: "finite ({InheritParent_file_type} \<union> {NormalFile_type t | t. t \<in> UNIV})" |
|
108 using p1 by auto |
|
109 have p3: "UNIV = ({InheritParent_file_type} \<union> {NormalFile_type t | t. t \<in> UNIV})" |
|
110 apply (rule set_eqI, auto split:t_rc_file_type.splits) |
|
111 by (case_tac x, auto) |
|
112 show ?thesis by (simp only:p3 p2) |
|
113 qed |
|
114 |
|
115 lemma finite_t_normal_proc_type: "finite (UNIV :: t_normal_proc_type set)" |
|
116 proof- |
|
117 have p1: "finite {CGI_P_proc c | c. c \<in> UNIV}" using finite_t_client by auto |
|
118 have p2: "finite ({CGI_P_proc c | c. c \<in> UNIV} \<union> {WebServer_proc})" using p1 by auto |
|
119 have p3: "UNIV = ({CGI_P_proc c | c. c \<in> UNIV} \<union> {WebServer_proc})" |
|
120 apply (rule set_eqI, auto split:t_normal_proc_type.splits) |
|
121 by (case_tac x, auto) |
|
122 show ?thesis by (simp only:p3 p2) |
|
123 qed |
|
124 |
|
125 lemma finite_t_rc_proc_type: "finite (UNIV :: t_rc_proc_type set)" |
|
126 proof- |
|
127 have p1: "finite {NormalProc_type t | t. t \<in> UNIV}" using finite_t_normal_proc_type by auto |
|
128 have p2: "finite ({NormalProc_type t | t. t \<in> UNIV} \<union> {InheritParent_proc_type, UseNewRoleType})" |
|
129 using p1 by auto |
|
130 have p3: "UNIV = ({NormalProc_type t | t. t \<in> UNIV} \<union> {InheritParent_proc_type, UseNewRoleType})" |
|
131 apply (rule set_eqI, auto split:t_rc_proc_type.splits) |
|
132 by (case_tac x, auto) |
|
133 show ?thesis by (simp only:p3 p2) |
|
134 qed |
|
135 |
|
136 lemma finite_t_normal_ipc_type : "finite (UNIV :: t_normal_ipc_type set)" |
|
137 proof- |
|
138 have p1: "finite {WebIPC}" by auto |
|
139 have p2: "UNIV = {WebIPC}" apply auto by (case_tac x, auto) |
|
140 show ?thesis by (simp only:p1 p2) |
|
141 qed |
|
142 |
|
143 definition |
|
144 "all_sps \<equiv> (UNIV ::t_normal_role set) \<times> (UNIV :: t_role set) \<times> (UNIV :: t_normal_proc_type set) \<times> init_users" |
|
145 |
|
146 lemma finite_all_sps: "finite all_sps" |
|
147 proof- |
|
148 have "finite ((UNIV :: t_normal_proc_type set) \<times> init_users)" |
|
149 using finite_t_normal_proc_type init_finite |
|
150 by (rule_tac finite_cartesian_product, auto) |
|
151 hence "finite ((UNIV :: t_role set) \<times> (UNIV :: t_normal_proc_type set) \<times> init_users)" |
|
152 using finite_t_role by (rule_tac finite_cartesian_product, auto) |
|
153 hence "finite ((UNIV::t_normal_role set) \<times> (UNIV::t_role set) \<times> (UNIV::t_normal_proc_type set) \<times> init_users)" |
|
154 using finite_t_normal_role by (rule_tac finite_cartesian_product, auto) |
|
155 thus ?thesis by (simp only:all_sps_def) |
|
156 qed |
|
157 |
|
158 definition |
|
159 "all_SPs \<equiv> {SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes} \<union> {SProc sp None | sp. sp \<in> all_sps}" |
|
160 |
|
161 lemma finite_all_SPs: "finite all_SPs" |
|
162 proof- |
|
163 have p1: "finite {SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes}" |
|
164 using finite_all_sps init_finite by auto |
|
165 have p2: "finite {SProc sp None | sp. sp \<in> all_sps}" |
|
166 using finite_all_sps by auto |
|
167 have "finite ({SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes} \<union> |
|
168 {SProc sp None | sp. sp \<in> all_sps})" |
|
169 using p1 p2 by auto |
|
170 thus ?thesis by (simp only:all_SPs_def) |
|
171 qed |
|
172 |
|
173 definition |
|
174 "all_sfs \<equiv> (UNIV :: t_normal_file_type set) \<times> init_files" |
|
175 |
|
176 lemma finite_all_sfs: "finite all_sfs" |
|
177 proof- |
|
178 have "finite ((UNIV :: t_normal_file_type set) \<times> init_files)" |
|
179 using finite_t_normal_file_type init_finite |
|
180 by (rule_tac finite_cartesian_product, auto) |
|
181 thus ?thesis by (simp add:all_sfs_def) |
|
182 qed |
|
183 |
|
184 definition |
|
185 "all_SFs \<equiv> {SFile sf (Some f) | sf f. sf \<in> all_sfs \<and> f \<in> init_files} \<union> {SFile sf None| sf. sf \<in> all_sfs}" |
|
186 |
|
187 lemma finite_all_SFs: "finite all_SFs" |
|
188 proof- |
|
189 have p1: "finite ({SFile sf (Some f) | sf f. sf \<in> all_sfs \<and> f \<in> init_files} \<union> |
|
190 {SFile sf None| sf. sf \<in> all_sfs})" |
|
191 using finite_all_sfs init_finite by auto |
|
192 thus ?thesis by (simp only:all_SFs_def) |
|
193 qed |
|
194 |
|
195 definition |
|
196 "all_SIs \<equiv> {SIPC si (Some i)| si i. si \<in> UNIV \<and> i \<in> init_ipcs} \<union> {SIPC si None| si. si \<in> UNIV}" |
|
197 |
|
198 lemma finite_all_SIs: "finite all_SIs" |
|
199 proof- |
|
200 have "finite ({SIPC si (Some i)| si i. si \<in> UNIV \<and> i \<in> init_ipcs} \<union> {SIPC si None| si. si \<in> UNIV})" |
|
201 using finite_t_normal_ipc_type init_finite by auto |
|
202 thus ?thesis by (simp only:all_SIs_def) |
|
203 qed |
|
204 |
|
205 lemma all_sobjs_srf_init': |
|
206 "sobj \<in> all_sobjs \<Longrightarrow> \<forall> sf srf. sobj = SFile sf (Some srf) \<longrightarrow> srf \<in> init_files" |
|
207 by (erule all_sobjs.induct, auto) |
|
208 |
|
209 lemma all_sobjs_srf_init: |
|
210 "SFile sf (Some srf) \<in> all_sobjs \<Longrightarrow> srf \<in> init_files" |
|
211 by (auto dest!:all_sobjs_srf_init') |
|
212 |
|
213 lemma all_sobjs_sd_init': |
|
214 "sobj \<in> all_sobjs \<Longrightarrow> \<forall> tf sd srf. sobj = SFile (tf, sd) srf \<longrightarrow> sd \<in> init_files" |
|
215 by (erule all_sobjs.induct, auto) |
|
216 |
|
217 lemma all_sobjs_sd_init: |
|
218 "SFile (tf, sd) srf \<in> all_sobjs \<Longrightarrow> sd \<in> init_files" |
|
219 by (auto dest!:all_sobjs_sd_init') |
|
220 |
|
221 lemma all_sobjs_sri_init': |
|
222 "sobj \<in> all_sobjs \<Longrightarrow> \<forall> si sri. sobj = SIPC si (Some sri) \<longrightarrow> sri \<in> init_ipcs" |
|
223 apply (erule all_sobjs.induct, auto) using init_ipc_has_type |
|
224 by (simp add:bidirect_in_init_def) |
|
225 |
|
226 lemma all_sobjs_sri_init: |
|
227 "SIPC si (Some sri) \<in> all_sobjs \<Longrightarrow> sri \<in> init_ipcs" |
|
228 by (auto dest!:all_sobjs_sri_init') |
|
229 |
|
230 lemma all_sobjs_sru_init'[rule_format]: |
|
231 "sobj \<in> all_sobjs \<Longrightarrow> \<forall> r fr pt u srp. sobj = SProc (r,fr,pt,u) srp \<longrightarrow> u \<in> init_users" |
|
232 using init_owner_valid |
|
233 by (erule_tac all_sobjs.induct, auto) |
|
234 |
|
235 lemma all_sobjs_sru_init: |
|
236 "SProc (r,fr,pt,u) srp \<in> all_sobjs \<Longrightarrow> u \<in> init_users" |
|
237 by (auto dest!:all_sobjs_sru_init') |
|
238 |
|
239 lemma unknown_not_in_all_sobjs': |
|
240 "sobj \<in> all_sobjs \<Longrightarrow> sobj \<noteq> Unknown" |
|
241 by (erule_tac all_sobjs.induct, auto) |
|
242 |
|
243 lemma unknown_not_in_all_sobjs: |
|
244 "Unknown \<in> all_sobjs \<Longrightarrow> False" |
|
245 using unknown_not_in_all_sobjs' by auto |
|
246 |
|
247 lemma finite_all_sobjs: "finite all_sobjs" |
|
248 proof- |
|
249 have p1: "finite (all_SPs \<union> all_SFs \<union> all_SIs)" |
|
250 using finite_all_SPs finite_all_SFs finite_all_SIs by auto |
|
251 have p2: "all_sobjs \<subseteq> (all_SPs \<union> all_SFs \<union> all_SIs)" |
|
252 apply (rule subsetI) |
|
253 using all_sobjs_sd_init all_sobjs_sri_init all_sobjs_srf_init all_sobjs_srp_init |
|
254 all_sobjs_sru_init unknown_not_in_all_sobjs |
|
255 by (case_tac x, auto simp:all_SPs_def all_SFs_def all_SIs_def all_sps_def all_sfs_def) |
|
256 show ?thesis |
|
257 apply (rule_tac B = "(all_SPs \<union> all_SFs \<union> all_SIs)" in finite_subset) |
|
258 using p1 p2 by auto |
|
259 qed |
|
260 |
|
261 lemma finite_tainted_s: |
|
262 "finite tainted_s" |
|
263 apply (rule_tac B = "all_sobjs" in finite_subset) |
|
264 apply (rule tainted_s_subset_all_sobjs) |
|
265 apply (rule finite_all_sobjs) |
|
266 done |
|
267 |
|
268 end |
|
269 |
|
270 end |