211 apply (case_tac prod1, case_tac prod2, simp) |
211 apply (case_tac prod1, case_tac prod2, simp) |
212 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
212 apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) |
213 apply (case_tac obj, simp_all split:option.splits if_splits) |
213 apply (case_tac obj, simp_all split:option.splits if_splits) |
214 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
214 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) |
215 apply (rule_tac x = "O_msg nat m" in exI) |
215 apply (rule_tac x = "O_msg nat m" in exI) |
216 apply (simp) |
216 apply (simp add:cm2smsg_def split:option.splits) |
217 |
217 done |
218 apply (case_tac obj, (simp split:option.splits if_splits)+) |
|
219 apply (erule conjE, drule_tac ) |
|
220 |
|
221 |
|
222 |
218 |
223 lemma has_inode_tainted_aux: |
219 lemma has_inode_tainted_aux: |
224 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
220 "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s" |
225 apply (erule tainted.induct) |
221 apply (erule tainted.induct) |
226 apply (auto intro:tainted.intros simp:has_same_inode_def) |
222 apply (auto intro:tainted.intros simp:has_same_inode_def) |