272 |
272 |
273 lemma finite_ci: "finite (current_ipcs s)" |
273 lemma finite_ci: "finite (current_ipcs s)" |
274 apply (induct s) defer apply (case_tac a) |
274 apply (induct s) defer apply (case_tac a) |
275 using init_finite by auto |
275 using init_finite by auto |
276 |
276 |
|
277 end |
|
278 |
|
279 context tainting_s_complete begin |
|
280 |
|
281 lemma init_notin_curf_deleted: |
|
282 "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s" |
|
283 by (induct s, simp, case_tac a, auto) |
|
284 |
|
285 lemma init_notin_curi_deleted: |
|
286 "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s" |
|
287 by (induct s, simp, case_tac a, auto) |
|
288 |
|
289 lemma init_notin_curp_deleted: |
|
290 "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s" |
|
291 by (induct s, simp, case_tac a, auto) |
|
292 |
|
293 lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files" |
|
294 by (induct f, auto split:if_splits) |
|
295 |
|
296 lemma source_proc_in_init: |
|
297 "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes" |
|
298 apply (induct s arbitrary:p, simp split:if_splits) |
|
299 apply (frule valid_os, frule valid_cons, case_tac a) |
|
300 by (auto split:if_splits) |
|
301 |
|
302 end |
|
303 |
|
304 context tainting_s_sound begin |
|
305 |
277 (*** properties of new-proc new-ipc ... ***) |
306 (*** properties of new-proc new-ipc ... ***) |
278 |
307 |
279 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a " |
308 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a " |
280 apply (erule finite.induct, simp) |
309 apply (erule finite.induct, simp) |
281 apply (rule ballI) |
310 apply (rule ballI) |
297 by (simp add:new_ipc_def nn_notin) |
326 by (simp add:new_ipc_def nn_notin) |
298 |
327 |
299 lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False" |
328 lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False" |
300 by (simp add:ni_notin_curi) |
329 by (simp add:ni_notin_curi) |
301 |
330 |
302 end |
|
303 |
|
304 context tainting_s_complete begin |
|
305 |
|
306 lemma init_notin_curf_deleted: |
|
307 "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s" |
|
308 by (induct s, simp, case_tac a, auto) |
|
309 |
|
310 lemma init_notin_curi_deleted: |
|
311 "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s" |
|
312 by (induct s, simp, case_tac a, auto) |
|
313 |
|
314 lemma init_notin_curp_deleted: |
|
315 "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s" |
|
316 by (induct s, simp, case_tac a, auto) |
|
317 |
|
318 lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s" |
331 lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s" |
319 using ni_notin_curi[where \<tau> = s] |
332 using ni_notin_curi[where \<tau> = s] |
320 by (drule_tac init_notin_curi_deleted, simp+) |
333 by (drule_tac init_notin_curi_deleted, simp+) |
321 |
334 |
322 lemma np_init_deled: "new_proc s \<in> init_processes \<Longrightarrow> deleted (Proc (new_proc s)) s" |
335 lemma np_init_deled: "new_proc s \<in> init_processes \<Longrightarrow> deleted (Proc (new_proc s)) s" |
323 using np_notin_curp[where \<tau> = s] |
336 using np_notin_curp[where \<tau> = s] |
324 by (drule_tac init_notin_curp_deleted, simp+) |
337 by (drule_tac init_notin_curp_deleted, simp+) |
325 |
338 |
326 lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files" |
|
327 by (induct f, auto split:if_splits) |
|
328 |
|
329 lemma source_proc_in_init: |
|
330 "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes" |
|
331 apply (induct s arbitrary:p, simp split:if_splits) |
|
332 apply (frule valid_os, frule valid_cons, case_tac a) |
|
333 by (auto simp:np_notin_curp split:if_splits) |
|
334 |
|
335 end |
|
336 |
|
337 context tainting_s_sound begin |
|
338 |
339 |
339 lemma len_fname_all: "length (fname_all_a len) = len" |
340 lemma len_fname_all: "length (fname_all_a len) = len" |
340 by (induct len, auto simp:fname_all_a.simps) |
341 by (induct len, auto simp:fname_all_a.simps) |
341 |
342 |
342 lemma ncf_notin_curf: "new_childf f s \<notin> current_files s" |
343 lemma ncf_notin_curf: "new_childf f s \<notin> current_files s" |
364 by (simp add:new_childf_def) |
365 by (simp add:new_childf_def) |
365 |
366 |
366 lemma clone_event_no_limit: |
367 lemma clone_event_no_limit: |
367 "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)" |
368 "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)" |
368 apply (rule vs_step) |
369 apply (rule vs_step) |
369 apply (auto intro:clone_no_limit split:option.splits |
370 apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp' |
370 dest:current_proc_has_role current_proc_has_type) |
371 dest:current_proc_has_role current_proc_has_type) |
371 done |
372 done |
372 |
373 |
373 |
374 |
374 end |
375 end |