262 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) |
262 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) |
263 where |
263 where |
264 "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" |
264 "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" |
265 |
265 |
266 lemma s2ss_included_sobj: |
266 lemma s2ss_included_sobj: |
267 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
267 "\<lbrakk>dalive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
268 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
268 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
269 |
269 |
|
270 fun init_dobj_related :: "t_sobject \<Rightarrow> t_dobject \<Rightarrow> bool" |
|
271 where |
|
272 "init_dobj_related (S_proc (pi, sec, fds) tag) (D_proc p') = (pi = Init p')" |
|
273 | "init_dobj_related (S_file sfs tag) (D_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
|
274 | "init_dobj_related (S_dir sf) (D_dir f) = (sfile_related sf f)" |
|
275 | "init_dobj_related _ _ = False" |
|
276 |
270 lemma init_ss_in_prop: |
277 lemma init_ss_in_prop: |
271 "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk> |
278 "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; dalive s obj; init_dobj_related sobj obj\<rbrakk> |
272 \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" |
279 \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" |
273 apply (simp add:init_ss_in_def init_ss_eq_def) |
280 apply (simp add:init_ss_in_def init_ss_eq_def) |
274 apply (erule bexE, erule conjE) |
281 apply (erule bexE, erule conjE) |
275 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) |
282 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) |
276 done |
283 done |