Permalink
Browse files

Name the introduction rule of `pre_bisimilarity`

  • Loading branch information...
jeltsch committed Feb 10, 2019
1 parent 4113000 commit 473836f49a4118370ba29fe5b72d4159fa28094e
@@ -557,11 +557,11 @@ private lemma proper_stop_scope_redundancy: "\<zero> \<sim>\<^sub>\<sharp> \<nu>
proof
show "\<zero> \<lesssim>\<^sub>\<sharp> \<nu> a. \<zero>"
using no_proper_transitions_from_stop
by (blast intro: proper.pre_bisimilarity.intros)
by (blast intro: proper.pre_bisimilarity)
next
show "\<nu> a. \<zero> \<lesssim>\<^sub>\<sharp> \<zero>"
using no_proper_transitions_from_new_channel_stop
by (blast intro: proper.pre_bisimilarity.intros)
by (blast intro: proper.pre_bisimilarity)
qed

lemma proper_scope_redundancy: "p \<sim>\<^sub>\<sharp> \<nu> a. p"
@@ -124,7 +124,7 @@ coinductive
and
bisimilarity :: "['process, 'process] \<Rightarrow> bool" (infix "\<sim>" 50)
where
"transfer (\<sim>) p q \<Longrightarrow> p \<lesssim> q" |
pre_bisimilarity: "transfer (\<sim>) p q \<Longrightarrow> p \<lesssim> q" |
"p \<sim> q \<equiv> p \<lesssim> q \<and> q \<lesssim> p"

subsubsection \<open>Symmetry\<close>

0 comments on commit 473836f

Please sign in to comment.