equal
deleted
inserted
replaced
79 "G \<in> program ==> |
79 "G \<in> program ==> |
80 D ok G <-> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))" |
80 D ok G <-> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))" |
81 apply (cut_tac distr_spec) |
81 apply (cut_tac distr_spec) |
82 apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def |
82 apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def |
83 Allowed_def ok_iff_Allowed) |
83 Allowed_def ok_iff_Allowed) |
84 apply (drule_tac [2] x = G and P = "%y. x \<notin> Acts(y)" in bspec) |
|
85 apply auto |
|
86 apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1]) |
84 apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1]) |
87 apply (auto intro: safety_prop_Inter) |
85 apply (auto intro: safety_prop_Inter) |
88 done |
86 done |
89 |
87 |
90 lemma (in distr) distr_Increasing_Out: |
88 lemma (in distr) distr_Increasing_Out: |