equal
deleted
inserted
replaced
263 |
263 |
264 lemma p2_is_Gets_correct [iff]: "Gets_correct p2" |
264 lemma p2_is_Gets_correct [iff]: "Gets_correct p2" |
265 by (auto simp: Gets_correct_def dest: p2_has_no_Gets) |
265 by (auto simp: Gets_correct_def dest: p2_has_no_Gets) |
266 |
266 |
267 lemma p2_is_one_step [iff]: "one_step p2" |
267 lemma p2_is_one_step [iff]: "one_step p2" |
268 by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> p2" for ev evs, auto) |
268 unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> p2" for ev evs, auto) |
269 |
269 |
270 lemma p2_has_only_Says' [rule_format]: "evs \<in> p2 \<Longrightarrow> |
270 lemma p2_has_only_Says' [rule_format]: "evs \<in> p2 \<Longrightarrow> |
271 ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)" |
271 ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)" |
272 by (erule p2.induct, auto simp: req_def pro_def) |
272 by (erule p2.induct, auto simp: req_def pro_def) |
273 |
273 |