|
1 theory tainted |
|
2 imports Main rc_theory os_rc deleted_prop obj2sobj_prop |
|
3 begin |
|
4 |
|
5 context tainting begin |
|
6 |
|
7 lemma tainted_is_valid: |
|
8 "obj \<in> tainted s \<Longrightarrow> valid s" |
|
9 by (erule tainted.induct, auto simp:vs_nil) |
|
10 |
|
11 lemma tainted_is_current: |
|
12 "obj \<in> tainted s \<Longrightarrow> exists s obj" |
|
13 apply (erule tainted.induct) |
|
14 apply (auto dest:valid_os) |
|
15 apply (drule seeds_in_init, case_tac obj, auto) |
|
16 done |
|
17 |
|
18 lemma nodel_tainted_exists: |
|
19 "\<lbrakk>no_del_event (s'@s); obj \<in> tainted s\<rbrakk> \<Longrightarrow> exists (s'@s) obj" |
|
20 apply (drule_tac obj = obj in nodel_imp_un_deleted) |
|
21 by (drule tainted_is_current, simp add:not_deleted_imp_exists') |
|
22 |
|
23 lemma t_remain_app: |
|
24 "\<lbrakk>obj \<in> tainted s'; no_del_event (s @ s'); valid (s @ s')\<rbrakk> |
|
25 \<Longrightarrow> obj \<in> tainted (s @ s')" |
|
26 apply (induct s, simp) |
|
27 apply (simp only:cons_app_simp_aux) |
|
28 apply (frule valid_cons, frule no_del_event_cons_D, simp) |
|
29 apply (rule t_remain, simp+) |
|
30 apply (drule tainted_is_current) |
|
31 apply (case_tac a, case_tac [!] obj, auto) |
|
32 done |
|
33 |
|
34 end |
|
35 |
|
36 context tainting_s_complete begin |
|
37 |
|
38 lemma unknown_notin_tainted_s': |
|
39 "sobj \<in> tainted_s \<Longrightarrow> sobj \<noteq> Unknown" |
|
40 apply (erule tainted_s.induct, auto) |
|
41 apply (drule seeds_in_init) |
|
42 apply (subgoal_tac "exists [] obj") |
|
43 apply (drule init_obj_has_sobj, simp+) |
|
44 apply (case_tac obj, simp+) |
|
45 done |
|
46 |
|
47 lemma unknown_notin_tainted_s: |
|
48 "Unknown \<in> tainted_s \<Longrightarrow> False" |
|
49 by (auto dest:unknown_notin_tainted_s') |
|
50 |
|
51 end |
|
52 |
|
53 end |