Session C2KA_DistributedSystems

Theory Stimuli

(*  Title:        C2KA Stimulus Structure
    Author:       Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019
    Maintainers:  Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca>
*)

section ‹Stimulus Structure \label{sec:stimulus_structure}›

text ‹
A stimulus constitutes the basis for behaviour. Because of this, each discrete, observable event 
introduced to a system, such as that which occurs through the communication among agents or from the 
system environment, is considered to be a stimulus which invokes a response from each system agent.

A \emph{stimulus structure} is an idempotent semiring~$\STIMstructure$ with a multiplicatively 
absorbing~$\Dstim$ and identity~$\Nstim$. Within the context of stimuli,~$\STIMset$ is a set of 
stimuli which may be introduced to a system. The operator~$\STIMplus$ is interpreted as a choice 
between two stimuli and the operator~$\STIMdot$ is interpreted as a sequential composition of two 
stimuli. The element~$\Dstim$ represents the \emph{deactivation stimulus} which influences all agents 
to become inactive and the element~$\Nstim$ represents the \emph{neutral stimulus} which has no influence 
on the behaviour of all agents. The natural ordering relation~$\STIMle$ on a stimulus structure~$\stim$ 
is called the sub-stimulus relation. For stimuli~$s,t \in \STIMset$, we write~$s \STIMle t$ and say 
that~$s$ is a sub-stimulus of~$t$ if and only if~$s \STIMplus t = t$. 
›

theory Stimuli
  imports Main
begin

text ‹
The class \emph{stimuli} describes the stimulus structure for \CCKAabbrv. We do not use 
Isabelle's built-in theories for groups and orderings to allow a different notation for the operations 
on stimuli to be consistent with~\cite{Jaskolka2015ab}.
›

class plus_ord =
  fixes leq::"'a  'a  bool" ("(_/ 𝒮 _)"  [51, 51] 50)
  fixes add::"'a  'a  'a" (infixl "" 65)
  assumes leq_def: "x 𝒮 y  x  y = y"
  and add_assoc: "(x  y)  z = x  (y  z)"
  and add_comm: "x  y = y  x"
begin

notation
  leq  ("'(≤')") and
  leq ("(_/ 𝒮 _)"  [51, 51] 50)

end

class stimuli = plus_ord +
  fixes seq_comp::"'a  'a  'a" (infixl "" 70)
  fixes neutral :: 'a ("𝔫")
  and deactivation :: 'a ("𝔡")
  and basic :: "'a set" ("𝒮a")
  assumes stim_idem [simp]: "x  x = x"
  and seq_nl [simp]: "𝔫  x = x"
  and seq_nr [simp]: "x  𝔫 = x"
  and add_zero [simp]: "𝔡  x = x"
  and absorbingl [simp]: "𝔡  x = 𝔡"
  and absorbingr [simp]: "x  𝔡 = 𝔡"
  and zero_not_basic: "𝔡  𝒮a"
begin 

lemma inf_add_S_right: "x 𝒮 y  x 𝒮 y  z"
  unfolding leq_def
  by (simp add: add_assoc [symmetric])

lemma inf_add_S_left: "x 𝒮 y  x 𝒮 z  y"
  by (simp add: add_comm inf_add_S_right)

lemma leq_refl [simp]: "x 𝒮 x"
  unfolding leq_def
  by simp

end

end

Theory CKA

(*  Title:        C2KA Behaviour Structure (Concurrent Kleene Algebra)
    Author:       Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019
    Maintainers:  Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca>
*)

section ‹Behaviour Structure \label{sec:behaviour_structure}›

text ‹
Hoare et al.~\cite{Hoare2011aa} presented the framework of Concurrent Kleene Algebra (\CKAabbrv) which captures the concurrent 
behaviour of agents. The framework of \CKAabbrv is adopted to describe agent behaviours in distributed 
systems. For a \CKAabbrv~$\CKAstructure$,~$\CKAset$ is a set of possible behaviours. The operator~$+$ is 
interpreted as a choice between two behaviours, the operator~$\CKAseq$ is interpreted as a sequential 
composition of two behaviours, and the operator~$\CKApar$ is interpreted as a parallel composition of 
two behaviours. The operators~$\CKAiterSeq{\,}$ and~$\CKAiterPar{\,}$ are interpreted as a finite sequential 
iteration and a finite parallel iteration of behaviours, respectively. The element~$0$ represents the 
behaviour of the \emph{inactive agent} and the element~$1$ represents the behaviour of the \emph{idle agent}. 
Associated with a \CKAabbrv~$\cka$ is a natural ordering relation~$\CKAle$ related to the semirings upon which the 
\CKAabbrv is built which is called the sub-behaviour relation. For behaviours~$a,b \in \CKAset$, we 
write~$a \CKAle b$ and say that~$a$ is a sub-behaviour of~$b$ if and only if~$a + b = b$.
›

theory CKA
  imports Main
begin

no_notation
rtrancl ("(_*)" [1000] 999)

notation
times (infixl "*" 70)
and less_eq  ("'(≤𝒦')") 
and less_eq  ("(_/ 𝒦 _)"  [51, 51] 50)

text ‹
The class \emph{cka} contains an axiomatisation of Concurrent Kleene Algebras and a selection of useful theorems.›

class join_semilattice = ordered_ab_semigroup_add +
  assumes leq_def: "x  y  x + y = y"
  and le_def: "x < y  x  y  x  y"
  and add_idem [simp]: "x + x = x"
begin

lemma inf_add_K_right: "a 𝒦 a + b"
  unfolding leq_def
  by (simp add:  add_assoc[symmetric])

lemma inf_add_K_left: "a 𝒦 b + a"
  by (simp only: add_commute, fact inf_add_K_right)

end

class dioid = semiring + one + zero + join_semilattice +
  assumes par_onel [simp]: "1 * x = x"
  and par_oner [simp]: "x * 1 = x"
  and add_zerol [simp]: "0 + x = x"
  and annil [simp]: "0 * x = 0"
  and annir [simp]: "x * 0 = 0"

class kleene_algebra = dioid + 
  fixes star :: "'a  'a" ("_*" [101] 100)
  assumes star_unfoldl: "1 + x * x* 𝒦 x*"  
  and star_unfoldr: "1 + x* * x 𝒦 x*"
  and star_inductl: "z + x * y 𝒦 y  x* * z 𝒦 y"
  and star_inductr: "z + y * x 𝒦 y  z * x* 𝒦 y"

class cka = kleene_algebra +
  fixes seq :: "'a  'a  'a" (infixl ";" 70)
  and seqstar :: "'a  'a" ("_;" [101] 100)
  assumes seq_assoc: "x ; (y ; z) = (x ; y) ; z"
  and seq_rident [simp]: "x ; 1 = x"
  and seq_lident [simp]: "1 ; x = x"
  and seq_rdistrib [simp]: "(x + y);z = x;z + y;z"
  and seq_ldistrib [simp]: "x;(y + z) = x;y + x;z"
  and seq_annir [simp]: "x ; 0 = 0"
  and seq_annil [simp]: "0 ; x = 0" 
  and seqstar_unfoldl: "1 + x ; x; 𝒦 x;"  
  and seqstar_unfoldr: "1 + x; ; x 𝒦 x;"
  and seqstar_inductl: "z + x ; y 𝒦 y  x; ; z 𝒦 y"
  and seqstar_inductr: "z + y ; x 𝒦 y  z ; x; 𝒦 y"
  and exchange: "(a*b) ; (c*d) 𝒦 (b;c) * (a;d)"
begin

interpretation cka: kleene_algebra plus less_eq less "1" "0" seq seqstar
  by (unfold_locales, simp_all add: seq_assoc seqstar_unfoldl seqstar_unfoldr seqstar_inductl seqstar_inductr)

lemma par_comm: "a * b = b * a"
proof -
  have "(b*a) ; (1*1) 𝒦 (a;1) * (b;1)" by (simp only:  exchange)
  hence "b * a 𝒦 a * b" by (simp)
  hence "a * b 𝒦 b * a  a * b  = b * a" by (rule antisym_conv)
  moreover have "a * b 𝒦 b * a" proof -
  have "(a*b) ; (1*1) 𝒦 (b;1) * (a;1)" by (rule  exchange)
    thus ?thesis  by (simp)
  qed
  ultimately show ?thesis by (auto)
qed

lemma exchange_2: "(a*b) ; (c*d) 𝒦 (a;c) * (b;d)"
proof -
  have "(b*a) ; (c*d) 𝒦 (a;c) * (b;d)" by (rule exchange)
  thus ?thesis by (simp add: par_comm)
qed

lemma seq_inf_par: "a ; b 𝒦 a * b" 
proof -
  have "(1*a) ; (1*b) 𝒦 (a;1) * (1;b)" by (rule exchange)
  thus ?thesis by simp
qed

lemma add_seq_inf_par: "a;b + b;a 𝒦 a*b"
proof -
  have "a;b 𝒦 a*b" by (rule seq_inf_par)
  moreover have "b;a 𝒦 b*a" by (rule seq_inf_par)
  ultimately have "a;b + b;a 𝒦 a*b + b*a" by (simp add: add_mono)
  thus ?thesis by (simp add: par_comm)
qed

lemma exchange_3: "(a*b) ; c 𝒦 a * (b;c)"
proof -
  have "(a*b) ; (1*c) 𝒦 (a;1) * (b;c)" by (rule exchange_2)
  thus ?thesis by simp
qed

lemma exchange_4: "a ; (b*c) 𝒦 (a;b) * c"
proof -
  have "(1*a) ; (b*c) 𝒦 (a;b) * (1;c)" by (rule exchange)
  thus ?thesis by simp
qed

lemma seqstar_inf_parstar: "a; 𝒦 a*"
proof -
  have "a ; a* 𝒦 a * a*" by (rule seq_inf_par)
  hence "1 + a ; a* 𝒦 1 + a * a*" by (simp add: add_left_mono)
  hence "1 + a ; a* 𝒦 a*" by (simp add: star_unfoldl order_trans)
  hence "a; ; 1 𝒦 a*" by (rule seqstar_inductl)
  thus ?thesis by simp
qed

end

end

Theory C2KA

(*  Title:        C2KA: Communicating Concurrent Kleene Algebra
    Author:       Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019
    Maintainers:  Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca>
*)

section ‹Communicating Concurrent Kleene Algebra \label{sec:ccka}›

text ‹
\CCKAabbrv extends the algebraic foundation of \CKAabbrv with the notions of semimodules and 
stimulus structures to capture the influence of stimuli on the behaviour of system agents.

A \CCKAabbrv is a mathematical system consisting of two semimodules which describe how a stimulus 
structure~$\stim$ and a \CKAabbrv~$\cka$ mutually act upon one another to characterize the response 
invoked by a stimulus on an agent behaviour as a next behaviour and a next stimulus. The 
\leftSemimodule{\stim}~$\ActSemimodule$ describes how the stimulus structure~$\stim$ acts upon the 
\CKAabbrv~$\cka$ via the mapping~$\actOp$. The mapping~$\actOp$ is called the \emph{next behaviour mapping} 
and it describes how a stimulus invokes a behavioural response from a given agent. From~$\ActSemimodule$, 
the next behaviour mapping~$\actOp$ distributes over~$+$ and~$\STIMplus$. Additionally, since~$\ActSemimodule$ 
is unitary, it is the case that the neutral stimulus has no influence on the behaviour of all agents and 
since~$\ActSemimodule$ is zero-preserving, the deactivation stimulus influences all agents to become inactive. 
The \rightSemimodule{\cka}~$\OutSemimodule$ describes how the \CKAabbrv~$\cka$ acts upon the stimulus 
structure~$\stim$ via the mapping~$\outOp$. The mapping~$\outOp$ is called the \emph{next stimulus mapping} 
and it describes how a new stimulus is generated as a result of the response invoked by a given stimulus on 
an agent behaviour. From~$\OutSemimodule$, the next stimulus mapping~$\outOp$ distributes over~$\STIMplus$ 
and~$+$. Also, since~$\OutSemimodule$ is unitary, it is the case that the idle agent forwards any stimulus that 
acts on it and since~$\OutSemimodule$ is zero-preserving, the inactive agent always generates the deactivation 
stimulus. A full account of \CCKAabbrv can be found in~\cite{Jaskolka2015ab,Jaskolka2013aa,Jaskolka2014aa}. 
›

theory C2KA
  imports CKA Stimuli
begin

no_notation
comp (infixl "" 55)
and rtrancl ("(_*)" [1000] 999)

text ‹
The locale \emph{c2ka} contains an axiomatisation of \CCKAabbrv  and some basic theorems relying on the 
axiomatisations of stimulus structures and \CKAabbrv provided in Sections~\ref{sec:stimulus_structure} 
and~\ref{sec:behaviour_structure}, respectively. We use a locale instead of a class in order to allow 
stimuli and behaviours to have two different types.
›

locale c2ka =
  fixes next_behaviour :: "'b::stimuli  'a::cka  'a" (infixr "" 75)
  and next_stimulus :: "('b::stimuli × 'a::cka)  'b" ("λ")
  assumes lsemimodule1 [simp]: "s  (a + b) = (s  a) + (s  b)"
  and lsemimodule2 [simp]: "(s  t)  a = (s  a) + (t  a)"
  and lsemimodule3 [simp]: "(s  t)  a = s  (t  a)"
  and lsemimodule4 [simp]: "𝔫  a = a"
  and lsemimodule5 [simp]: "𝔡  a = 0"
  and rsemimodule1 [simp]: "λ(s  t, a) = λ(s, a)  λ(t, a)"
  and rsemimodule2 [simp]: "λ(s, a + b) = λ(s, a)  λ(s, b)"
  and rsemimodule3 [simp]: "λ(s, a ; b) = λ(λ(s, a), b)"
  and rsemimodule4 [simp]: "λ(s, 1) = s"
  and rsemimodule5 [simp]: "λ(s, 0) = 𝔡"
  and cascadingaxiom [simp]: "s  (a ; b) = (s  a);(λ(s, a)  b)"
  and cascadingoutputlaw: "a 𝒦 c  b = 1  (s  a);(λ(s,c)  b) = 0"
  and sequentialoutputlaw [simp]: "λ(s  t, a) = λ(s, ta)  λ(t, a)"
  and onefix: "s = 𝔡  s  1 = 1"
  and neutralunmodified: "a = 0  λ(𝔫, a) = 𝔫"
begin

text ‹
Lemmas \emph{inf-K-S-next-behaviour} and \emph{inf-K-S-next-stimulus} show basic results from the axiomatisation of \CCKAabbrv.
›

lemma inf_K_S_next_behaviour: "(a 𝒦 b  s 𝒮 t)  (s  a 𝒦 t  b)"
  unfolding Stimuli.leq_def CKA.leq_def
proof -
  assume hyp: "a + b = b  s  t = t"
  hence "s  a + t  b = s  a + (s  t)  b" by simp
  hence "s  a + t  b = s  a + s  b + t  b" by (simp add: algebra_simps)
  moreover have "s  (a + b) = s  a + s  b" by simp
  ultimately have "s  a + t  b = s  (a + b) + t  b" by simp
  hence "s  a + t  b = s  b + t  b" by (simp add: hyp)
  hence "s  a + t  b = (s  t)  b" by simp
  thus "s  a + t  b = t  b" by (simp add: hyp)
qed

lemma inf_K_S_next_stimulus: "a 𝒦 b  s 𝒮 t  λ(s,a) 𝒮 λ(t,b)"
  unfolding Stimuli.leq_def CKA.leq_def
proof -
  assume hyp: "a + b = b  s  t = t"
  hence "λ(s,a)  λ(t,b) = λ(s,a)  λ(st,b)" by simp
  hence "λ(s,a)  λ(t,b) = λ(s,a)  λ(s,b)  λ(t,b)" by (simp add: add_assoc)
  moreover have "λ(s,a+b) = λ(s,a)  λ(s,b)" by simp
  ultimately have "λ(s,a)  λ(t,b) = λ(s,a+b)  λ(t,b)" by simp
  hence "λ(s,a)  λ(t,b) = λ(s,b)  λ(t,b)" by (simp add: hyp)
  hence "λ(s,a)  λ(t,b) = λ(st,b)" by simp
  thus "λ(s,a)  λ(t,b) = λ(t,b)" by (simp add: hyp)
qed

text ‹
The following lemmas show additional results from the axiomatisation of \CCKAabbrv which follow from lemmas \emph{inf-K-S-next-behaviour} and \emph{inf-K-S-next-stimulus}.
›

lemma inf_K_next_behaviour: "a 𝒦 b  s  a 𝒦 s  b"
  by (simp add: inf_K_S_next_behaviour)

lemma inf_S_next_behaviour: "s 𝒮 t  s  a 𝒦 t  a"
  by (simp add: inf_K_S_next_behaviour)

lemma inf_add_seq_par_next_behaviour: "s  (a;b + b;a) 𝒦 s  (a*b)"
  using inf_K_next_behaviour add_seq_inf_par by blast

lemma inf_seqstar_parstar_next_behaviour: "s  a; 𝒦 s  a*"
  by (simp add: seqstar_inf_parstar inf_K_next_behaviour)

lemma inf_S_next_stimulus: "s 𝒮 t  λ(s,a) 𝒮 λ(t,a)"
  by (simp add: inf_K_S_next_stimulus)

lemma inf_K_next_stimulus: "a 𝒦 b  λ(s,a) 𝒮 λ(s,b)"
  by (simp add: inf_K_S_next_stimulus)

lemma inf_add_seq_par_next_stimulus: "λ(s, a;b + b;a) 𝒮 λ(s, a*b)"
proof -
  have "a;b 𝒦 a*b" by (rule seq_inf_par)
  moreover have "b;a 𝒦 b*a" by (rule seq_inf_par)
  ultimately have "a;b + b;a 𝒦 a*b + b*a" by (simp add: add_mono)
  hence "a;b + b;a 𝒦 a*b" by (simp add: par_comm)
  thus "λ(s, a;b + b;a) 𝒮 λ(s, a*b)" by (rule inf_K_next_stimulus)
qed

lemma inf_seqstar_parstar_next_stimulus: "λ(s, a;) 𝒮 λ(s, a*)"
  by (simp add: seqstar_inf_parstar inf_K_next_stimulus)

end

end

Theory Topology_C2KA

(*  Title:        Notions of Topology for C2KA
    Author:       Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019
    Maintainers:  Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca>
*)

section ‹Notions of Topology for \CCKAabbrv \label{sec:topology}›

text ‹
Orbits, stabilisers, and fixed points are notions that allow us to perceive a kind of topology of a system 
with respect to the stimulus-response relationships among system agents. In this context, the term ``topology'' 
is used to capture the relationships (influence) and connectedness via stimuli of the agents in a distributed 
system. It intends to capture a kind of reachability in terms of the possible behaviours for a given agent.

A \CCKAabbrv consists of two semimodules~$\ActSemimodule$ and~$\OutSemimodule$ for which we have a 
\leftAct{\stim}~$\lSact$ and a \rightAct{\cka}~$\rKact$. Therefore, there are two complementary notions of orbits, 
stabilisers, and fixed points within the context of agent behaviours and stimuli, respectively. In this way, one 
can use these notions to think about distributed systems from two different perspectives, namely the behavioural 
perspective provided by the action of stimuli on agent behaviours described by~$\ActSemimodule$ and the external 
event (stimulus) perspective provided by the action of agent behaviours on stimuli described by~$\OutSemimodule$. 
In this section, only the treatment of these notions with respect to the \leftSemimodule{\stim}~$\ActSemimodule$ 
and agent behaviours is provided. The same notions for the \rightSemimodule{\cka}~$\OutSemimodule$ and stimuli 
can be provided in a very similar way.

When discussing the interplay between \CCKAabbrv and the notions of orbits, stabilisers, and fixed points, the 
partial order of sub-behaviours~$\CKAle$ is extended to sets in order to express sets of agent behaviours 
encompassing one another. For two subsets of agent behaviours~$A,B \STleq \CKAset$, we say that~$A$ 
\emph{is encompassed by}~$B$ (or~$B$ \emph{encompasses}~$A$), written~$\CKAencompass{A}{B}$, if and only 
if~$\biglnotation{\forall}{a}{a \in A}{\lnotation{\exists}{b}{b \in B}{a \CKAle b}}$. In essence,~$A \CKAenc B$ 
indicates that every behaviour contained within the set~$A$ is a sub-behaviour of at least one behaviour in the 
set~$B$. The encompassing relation~$\STIMenc$ for stimuli can be defined similarly. 

Throughout this section, let~$\ActSemimodule$ be the unitary and zero-preserving \leftSemimodule{\stim} of a 
\CCKAabbrv and let~$a \in \CKAset$.
›

theory Topology_C2KA
  imports C2KA
begin

no_notation
comp (infixl "" 55)
and rtrancl ("(_*)" [1000] 999)

text ‹
The locale \emph{topology-c2ka} extends the axiomatisation of \emph{c2ka} to support the notions of topology. 
›

locale topology_c2ka = c2ka +
  fixes orbit :: "'a::cka  'a::cka set" ("Orb")
  and strong_orbit :: "'a::cka  'a::cka set" ("OrbS")
  and stabiliser :: "'a::cka  'b::stimuli set" ("Stab")
  and fixed :: "'a::cka  bool"
  and encompassing_relation_behaviours :: "'a set  'a set  bool"  (infix "𝒦" 50)
  and encompassing_relation_stimuli :: "'b set  'b set  bool"  (infix "𝒮" 50)
  and induced :: "'a::cka  'a::cka  bool" (infix "" 50)
  and orbit_equivalent :: "'a::cka  'a::cka  bool" (infix "𝒦" 50)
  assumes orb_def: "x  Orb(a)  (s. (s  a = x))"
  and orbs_def: "b  OrbS(a)  Orb(b) = Orb(a)"
  and stab_def: "s  Stab(a)  s  a = a"
  and fixed_def: "fixed(a)  (s::'b. s𝔡  s  a = a)"
  and erb_def: "A 𝒦 B  (a::'a. a  A  (b. b  B  a 𝒦 b))"
  and ers_def: "E 𝒮 F  (a::'b. a  E  (b. b  F  a 𝒮 b))"
  and induced_def: "a  b  b  Orb(a)"
  and orbit_equivalent_def: "a 𝒦 b  Orb(a) = Orb(b)"
begin

subsection ‹Orbits \label{sub:orbits}›

text ‹
The \emph{orbit} of~$a$ in~$\stim$ is the set given by~$\orb{a} = \sets{\lAct{a}{s}}{s \in \STIMset}$. The orbit of 
an agent~$a \in \CKAset$ represents the set of all possible behavioural responses from an agent behaving as~$a$ to 
any stimulus from~$\stim$. In this way, the orbit of a given agent can be perceived as the set of all possible 
future behaviours for that agent. 
›


text ‹
Lemma \emph{inf-K-enc-orb} provides an isotonicity law with respect to the orbits and the encompassing relation for agent behaviours.
›

lemma inf_K_enc_orb: "a 𝒦 b  Orb(a) 𝒦 Orb(b)"
  unfolding erb_def orb_def
  using inf_K_next_behaviour by blast
  
text ‹
The following lemmas provide a selection of properties regarding orbits and the encompassing relation for agent behaviours.
›

lemma enc_orb_add: "Orb(a) 𝒦 Orb(a + b)"
  using  inf_K_enc_orb inf_add_K_right by auto

lemma enc_orb_exchange: "Orb((a*b) ; (c*d)) 𝒦 Orb((a;c) * (b;d))"
  using inf_K_enc_orb exchange_2 by blast

lemma enc_orb_seq_par: "Orb(a;b) 𝒦 Orb(a*b)"
  using inf_K_enc_orb seq_inf_par by auto

lemma enc_orb_add_seq_par: "Orb(a;b + b;a) 𝒦 Orb(a*b)"
  using inf_K_enc_orb add_seq_inf_par by auto

lemma enc_orb_parseq: "Orb((a*b);c) 𝒦 Orb(a*(b;c))"
  using inf_K_enc_orb exchange_3 by blast

lemma enc_orb_seqpar: "Orb(a;(b*c)) 𝒦 Orb((a;b)*c)"
  using inf_K_enc_orb exchange_4 by blast

lemma enc_orb_seqstar_parstar: "Orb(a;) 𝒦 Orb(a*)"
  using inf_K_enc_orb seqstar_inf_parstar by auto

lemma enc_orb_union: "Orb(a) 𝒦 Orb(c)  Orb(b) 𝒦 Orb(c) 
 Orb(a)  Orb(b) 𝒦  Orb(c)"
  unfolding erb_def 
  by auto
   
subsection ‹Stabilisers \label{sub:stabilisers}›

text ‹
The \emph{stabiliser} of~$a$ in~$\stim$ is the set given by~$\stab{a} = \sets{s \in \STIMset}{\lAct{a}{s} = a}$. 
The stabiliser of an agent~$a \in \CKAset$ represents the set of stimuli which have no observable influence 
(or act as neutral stimuli) on an agent behaving as~$a$.
›  

text ‹
Lemma \emph{enc-stab-inter-add} provides a property regarding stabilisers and the encompassing relation for stimuli.
›

lemma enc_stab_inter_add: "Stab(a)  Stab(b) 𝒮 Stab(a + b)"
  unfolding ers_def
  by (auto simp add: stab_def, rename_tac s, rule_tac x="s" in exI, simp)
  
subsection ‹Fixed Points \label{sub:fixed_points}›

text ‹
An element~$a \in \CKAset$ is called a \emph{fixed point} if~$\lnotation{\forall}{s}{s \in \STIMset \STdiff \set{\Dstim}}{\lAct{a}{s} = a}$.\linebreak 
When an agent behaviour is a fixed point, it is not influenced by any stimulus other than the deactivation stimulus~$\Dstim$. 
It is important to note that since~$\ActSemimodule$ is zero-preserving, every agent behaviour becomes inactive when subjected to the 
deactivation stimulus~$\Dstim$. Because of this, we exclude this special case when discussing fixed point agent behaviours.
›  

lemma zerofix [simp]: "s  0 = 0"
proof -
  have "0 = 𝔡  a" by simp
  hence "s  0 = s  (𝔡  a)" by simp
  hence "s  0 = (s  𝔡)  a" by (simp only: lsemimodule3 [symmetric])
  thus "s  0 = 0" by simp
qed

text ‹
The following lemmas provide a selection of properties regarding fixed agent behaviours.
›  

lemma fixed_zero: "fixed(0)"
  unfolding fixed_def
  by simp

lemma fixed_a_b_add: "fixed(a)  fixed(b)  fixed(a + b)"
  unfolding fixed_def
  by simp

lemma fix_not_deactivation: "s  a = a  λ(s,a) = 𝔡  a = 0"
proof -
  assume E: "s  a = a  λ(s,a) = 𝔡"
  hence "s  (a;1) = a" by simp
  hence "(sa) ; (λ(s,a)1) = a" by (simp only: cascadingaxiom)
  hence "0 = a" by (simp add: E)
  thus ?thesis by auto
qed

lemma fixed_a_b_seq: "fixed(a)  fixed(b)  fixed(a ; b)"
  unfolding fixed_def
proof (rule impI)
  assume hyp: "(s. s  𝔡  s  a = a)  (s. s  𝔡  s  b = b)"
  have C1: "(s. λ(s,a) = 𝔡  s  𝔡  s  (a ; b) = a ; b)"
  proof -
    have E: "(s. s  𝔡  λ(s,a) = 𝔡  s  (a ; b) = 0)" by simp
    hence "(s. s  𝔡  λ(s,a) = 𝔡  s  a = a  λ(s,a) = 𝔡)" 
      by (simp add: hyp)
    moreover have "(s. s  a = a  λ(s,a) = 𝔡  a = 0)" 
      by (simp add: fix_not_deactivation)
    ultimately have "(s. s  𝔡  λ(s,a) = 𝔡  a = 0)" by auto
    thus ?thesis by (auto simp add: E)
  qed
  moreover have C2: "(s. λ(s,a)  𝔡  s  𝔡  s  (a ; b) = a ; b)" 
    by (simp add: hyp)
  ultimately show "(s. s  𝔡  s  (a ; b) = a ; b)" by blast
qed

subsection ‹Strong Orbits and Induced Behaviours \label{sub:strong_orbits_and_induced_behaviours}›

text ‹
The \emph{strong orbit} of~$a$ in~$\stim$ is the set given by~$\orbS{a} = \sets{b \in \CKAset}{\orb{b} = \orb{a}}$. 
Two agents are in the same strong orbit, denoted~$a \CKAsim b$ for~$a,b \in \CKAset$, if and only if their orbits are 
identical. This is to say when~$a \CKAsim b$, if an agent behaving as~$a$ is influenced by a stimulus to behave as~$b$, 
then there exists a stimulus which influences the agent, now behaving as~$b$, to revert back to its original behaviour~$a$. 

The influence of stimuli on agent behaviours is called the \emph{induced behaviours} via stimuli. Let~$a,b \in \CKAset$ 
be agent behaviours with~$a \neq b$. We say that~$b$ is \emph{induced by~$a$ via stimuli} (denoted by~$\induced{b}{a}$) 
if and only if~$\lnotation{\exists}{s}{s \in \STIMset}{\lAct{a}{s} = b}$. The notion of induced behaviours allows us to make 
some predictions about the evolution of agent behaviours in a given system by providing some insight into how different agents 
can respond to any stimuli.
›  

text ‹
Lemma \emph{fixed-not-induce} states that if an agent has a fixed point behaviour, then it does not induce any agent behaviours via  stimuli besides the inactive behaviour~$0$.
›  

lemma fixed_not_induce: "fixed(a)  (b. b  0  b  a  ¬(a  b))"
proof -
  have "s. s = 𝔡  s  𝔡  (t. t  𝔡  t  a = a)  s  a  0 
 s  a  a  False"
    by (erule disjE, simp_all)
  hence "s. (t. t  𝔡  t  a = a)  s  a  0  s  a  a  False"
    by simp
  thus ?thesis 
    unfolding fixed_def induced_def orb_def
    by auto
qed

text ‹
Lemma \emph{strong-orbit-both-induced} states that all agent behaviours which belong to the same strong orbit are mutually induced via some (possibly different) stimuli.
This is to say that if two agent behaviours are in the same strong orbit, then there exists inverse stimuli for each agent behaviour in a 
strong orbit allowing an agent to revert back to its previous behaviour.
›  

lemma in_own_orbit: "a  Orb(a)"
  unfolding orb_def
  by (rule_tac x="𝔫" in exI, simp)

lemma strong_orbit_both_induced: "a 𝒦 b  a  b  b  a"
  unfolding orbit_equivalent_def induced_def
  by (blast intro: in_own_orbit)

text ‹
Lemma \emph{strong-orbit-induce-same} states that if two agent behaviours are in the same strong orbit, then a third behaviour can be induced via  stimuli by either of 
the behaviours within the strong orbit. This is to say that each behaviour in a strong orbit can induce the same set of behaviours
(perhaps via different stimuli).
›  

lemma strong_orbit_induce_same: "a 𝒦 b  (a  c  b  c)"
  unfolding induced_def orbit_equivalent_def
  by simp

end

end

Theory Communication_C2KA

(*  Title:        Notions of Communication for C2KA
    Author:       Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019
    Maintainers:  Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca>
*)

section ‹Notions of Communication for \CCKAabbrv \label{sec:communication}›

text ‹
Distributed systems contain a significant number of interactions among their constituent agents. Any interaction, 
direct or indirect, of an agent with its neighbouring agents can be understood as a \emph{communication}~\cite{Milner1989aa}. 
Therefore, any potential for communication between two system agents can be characterized by the existence of a communication 
path allowing for the transfer of data or control from one agent to another. Potential for communication allows system
agents to have an \emph{influence} over each other. The study of agent influence allows for the 
determination of the overall structure of the distributed system of which the agents comprise. A full treatment of the potential 
for communication within distributed systems specified using \CCKAabbrv has been given in~\cite{Jaskolka2015ab} 
and~\cite{Jaskolka2014ac} and is highlighted below.

Consider a distributed system with~$\Agent{A}, \Agent{B} \in \A$ such that~$\Agent{A} \neq \Agent{B}$. We write~$\agent{A}{a}$ 
where~$\Agent{A}$ is the name given to the agent and~$a \in \CKAset$ is the agent behaviour. For~$\agent{A}{a}$ and~$\agent{B}{b}$, 
we write~$\Agent{A+B}$ to denote the agent~$\bigA{a+b}$. In a sense, we extend the operators on behaviours of~$\CKAset$ to their 
corresponding agents. 

Communication via stimuli from agent~$\Agent{A}$ to agent~$\Agent{B}$ is said to have taken place only when 
a stimulus generated by~$\Agent{A}$ \emph{influences} (i.e., causes an observable change in, directly or indirectly) the behaviour 
of~$\Agent{B}$. Note that it is possible that more than one agent is influenced by the generation of the same stimulus by another 
agent in the system. Formally, we say that agent~$\agent{A}{a}$ has the \emph{potential for direct communication via stimuli} with 
agent~$\agent{B}{b}$ (denoted by~$\STIMcommD{\Agent{A}}{\Agent{B}}$) if and only 
if~$\biglnotation{\exists}{s,t}{s,t \in \STIMbasic \nAnd t \STIMle \lOut{a}{s} }{\lAct{b}{t} \neq b}$ where~$\STIMbasic$ is the 
set of all basic stimuli. A stimulus is called \emph{basic} if it is indivisible with regard to the sequential composition 
operator~$\STIMdot$ of a stimulus structure. Similarly, we say that agent~$\Agent{A}$ has the \emph{potential for communication 
via stimuli with agent~$\Agent{B}$ using at most~$n$ basic stimuli} (denoted by~$\STIMcommN{\Agent{A}}{\Agent{B}}{n}$) if and only 
if~$\biglnotation{\exists}{\Agent{C}}{\Agent{C} \in \A \nAnd \Agent{C} \neq \Agent{A} \nAnd \Agent{C} \neq \Agent{B}}{\STIMcommN{\Agent{A}}{\Agent{C}}{(n-1)} \nAnd \STIMcommD{\Agent{C}}{\Agent{B}}}$. 
More generally, we say that agent~$\Agent{A}$ has the \emph{potential for communication via stimuli} with agent~$\Agent{B}$ 
(denoted by~$\STIMcomm{\Agent{A}}{\Agent{B}}$) if and only if~$\biglnotation{\exists}{n}{n \ge 1}{\STIMcommN{\Agent{A}}{\Agent{B}}{n}}$. 
When~$\STIMcomm{\Agent{A}}{\Agent{B}}$, there is a sequence of stimuli of arbitrary length which allows for the transfer of data or 
control from agent~$\Agent{A}$ to agent~$\Agent{B}$ in the system. To simplify the Isabelle theory, we do not implement 
the potential for communication using at most~$n$ basic stimuli. Instead, we give the definition of potential for direct communication 
via stimuli and the fact that~$\STIMcommD{\Agent{A}}{\Agent{B}} \Longrightarrow \STIMcomm{\Agent{A}}{\Agent{B}}$ as axioms because 
these are the only properties that we use about potential for communication via stimuli.

Communication via shared environments from agent~$\Agent{A}$ to agent~$\Agent{B}$ (denoted by~$\ENVcomm{\Agent{A}}{\Agent{B}}$) is 
said to have taken place only when~$\Agent{A}$ has the ability to alter an element of the environment that it shares with~$\Agent{B}$ 
such that~$\Agent{B}$ is able to observe the alteration that was made. Formally, we say that agent~$\agent{A}{a}$ has the 
\emph{potential for direct communication via shared environments} with agent~$\agent{B}{b}$ (denoted by~$\ENVcommD{\Agent{A}}{\Agent{B}}$) 
if and only if~$\dep{b}{a}$ where~$\depOp$ is a given dependence relation. More generally, agent~$\Agent{A}$ has the 
\emph{potential for communication via shared environments} with agent~$\Agent{B}$ (denoted by~$\ENVcomm{\Agent{A}}{\Agent{B}}$) if and 
only if~$\depTC{b}{a}$ where~$\depOpTC$ is the transitive closure of the given dependence relation. This means that if two agents respect 
the given dependence relation, then there is a potential for communication via shared environments.
›

theory Communication_C2KA
  imports Topology_C2KA
begin

text ‹
The locale \emph{communication-c2ka} extends \emph{topology-c2ka} to include aspects of potential for communication 
among distributed system agents.
›

locale communication_c2ka = topology_c2ka +
  fixes dcs :: "'a::cka  'a::cka  bool" (infix "𝒮" 50)
  and pcs :: "'a::cka  'a::cka  bool" (infix "𝒮+" 50)
  and dce :: "'a::cka  'a::cka  bool" (infix "" 50)
  and pce :: "'a::cka  'a::cka  bool" (infix "+" 50)
  and pdc :: "'a::cka  'a::cka  bool" (infix "" 50)
  and pfc :: "'a::cka  'a::cka  bool" (infix "+" 50)
  and stimuli_connected :: "'a set  bool"
  and universally_influential :: "'a::cka × 'a set  bool"
  assumes dcs_def: "a 𝒮 b  
  ( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,a)  t  b  b)"
  and pdc_def: "a  b  (a 𝒮 b  a  b)"
  and zero_dce: "¬(0  a)"
  and one_dce: "¬(1  a)"
  and dce_zero: "¬(a  0)"
  and dce_one: "¬(a  1)"
  and sum_dce: "(A + B  C)  (A  C  B  C)"
  and dce_sum: "(A  B + C)  (A  B  A  C)"
  and dcs_pcs: "A 𝒮 B  A 𝒮+ B"
  and stimuli_connected_def: "stimuli_connected(𝒞)  
( X1 X2. X1  X2 = {}  X1  X2 = 𝒞  X1  {}  X2  {}  
( A B. A  X1  B  X2  (A 𝒮+ B  B 𝒮+ A)))"
  and universally_influential_def: "universally_influential(A,𝒞) 
A  𝒞  ( B. B  𝒞  B  A  A 𝒮+ B)"
begin

subsection ‹Stimuli-Connected Systems \& Universally Influential Agents \label{sub:stimuli_connected_universally_influential}›

text ‹
Two subsets~$X_1$ and~$X_2$ of~$\A$ form a partition of~$\A$ if and only if~$X_1 \cap X_2 = \STbot$ and~$X_1 \cup X_2 = \A$. A distributed system 
of agents~$\A$ is called \emph{stimuli-connected} if and only if for every~$X_1$ and~$X_2$ nonempty that form a partition of~$\A$, we 
have~$\lnotation{\exists}{\Agent{A},\Agent{B}}{\Agent{A} \in X_1 \nAnd \Agent{B} \in X_2}{\STIMcomm{\Agent{A}}{\Agent{B}} \Ors \STIMcomm{\Agent{B}}{\Agent{A}}}$. 
Otherwise,~$\A$ is called \emph{stimuli-disconnected}. In a stimuli-connected system, every agent is a participant, either as the source or sink, 
of at least one direct communication via stimuli.
›

text ‹
An agent~$\Agent{A} \in \A$ is called \emph{universally influential} if and only 
if~$\biglnotation{\forall}{\Agent{B}}{\Agent{B} \in \A \STdiff \set{\Agent{A}}}{\STIMcomm{\Agent{A}}{\Agent{B}}}$. 
A universally influential agent is able to generate some stimuli that influences the behaviour, either directly or 
indirectly, of each other agent in the system. 
›

text ‹
Lemma \emph{universally-influential-stimuli-connected} shows that the existence of a universally influential agent yields a stimuli-connected system. 
›

lemma universally_influential_stimuli_connected: 
"( A. universally_influential(A,𝒞))  stimuli_connected(𝒞)"
  unfolding universally_influential_def stimuli_connected_def
proof (intro allI impI)
  fix X1 X2
  show "(A. A  𝒞  (B. B  𝒞  B  A  A 𝒮+ B)) 
X1  X2 = {}  X1  X2 = 𝒞  X1  {}  X2  {}  
( A B. A  X1  B  X2  (A 𝒮+ B  B 𝒮+ A))"
  proof -
    assume "(A. A  𝒞  (B. B  𝒞  B  A  A 𝒮+ B))"
    from this obtain A where Aui: "A  𝒞  (B. B  𝒞  B  A  
A 𝒮+ B)" by auto
    show "X1  X2 = {}  X1  X2 = 𝒞  X1  {}  X2  {} 
(A B. A  X1  B  X2  (A 𝒮+ B  B 𝒮+ A))"
    proof -
      assume partition:"X1  X2 = {}  X1  X2 = 𝒞  X1  {}  X2  {}"
      show "(A B. A  X1  B  X2  (A 𝒮+ B  B 𝒮+ A))"
      proof cases 
        assume in1: "A  X1"
        from partition obtain B where in2: "B  X2" by auto
        have "A = B  False"
        proof -
          assume "A = B"
          hence "A  X2" by (simp add: in2)
          moreover have "A  X1" by (rule in1)
          ultimately have "A  X1  X2" by simp
          hence "A  {}" by (simp add: partition)
          thus "False" by simp
        qed
        hence "A  B" by auto
        moreover have "B  𝒞" 
        proof -
          from partition have "𝒞 = X1  X2" by auto
          hence "X2  𝒞" by simp
          thus ?thesis by (auto simp add: in2)
        qed
        ultimately have "A 𝒮+ B" by (auto simp add: Aui in2)
        thus ?thesis 
          by (rule_tac x="A" in exI, rule_tac x="B" in exI, simp add: in1 in2)
      next
        assume notin1: "A  X1"
        moreover have "A  𝒞" by (simp add: Aui)
        moreover have "X1  X2 = 𝒞" by (simp add: partition)
        ultimately have in2: "A  X2" by auto
        from partition obtain B where in1: "B  X1" by auto
        have "B = A  False"
        proof -
          assume "B = A"
          hence "B  X2" by (simp add: in2)
          moreover have "B  X1" by (rule in1)
          ultimately have "B  X1  X2" by simp
          hence "B  {}" by (simp add: partition)
          thus "False" by simp
        qed
        hence "B  A" by auto
        moreover have "B  𝒞" 
        proof -
          from partition have "𝒞 = X1  X2" by auto
          hence "X1  𝒞" by simp
          thus ?thesis by (auto simp add: in1)
        qed
        ultimately have "A 𝒮+ B" by (auto simp add: Aui in2)
        thus ?thesis 
          by (rule_tac x="B" in exI, rule_tac x="A" in exI, simp add: in1 in2)
      qed
    qed
  qed
qed

text ‹
Lemma \emph{fixed-no-stimcomm} shows that no agent has the potential for communication via stimuli with an agent that has a fixed point behaviour.
›

lemma fixed_no_stimcomm: "fixed(A)  ( B. ¬(B 𝒮 A))"
  unfolding fixed_def 
proof (rule impI)
  assume hyp: "s. s  𝔡  s  A = A"
  have " B. B 𝒮 A  False"
  proof -
    assume " B. B 𝒮 A"
    then obtain B where "B 𝒮 A" by auto
    hence " s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,B)  t  A  A" 
      by (simp only: dcs_def)
    then obtain s t where st: "s  𝒮a  t  𝒮a  t 𝒮 λ(s,B)  t  A  A" 
      by auto
    hence "t  𝔡" by (auto simp only: zero_not_basic)
    hence "t  A = A" by (simp add: hyp)
    thus False by (auto simp add: st)
  qed
  thus "( B. ¬(B 𝒮 A))" by auto
qed

subsection ‹Preserving the Potential for Communication under Non-Determinism \label{sub:non_determinism}›

subsubsection ‹Potential for Communication via Stimuli \label{ssub:pfc_stim}›

text ‹
The following results show how the potential for communication via stimuli can be preserved when non-determinism is introduced among agents. 
Specifically, Lemma \emph{source-nondet-stimcomm} states that when non-determinism is added at the source of a potential communication path via stimuli, the potential 
for communication via stimuli is always preserved. On the other hand, Lemma \emph{sink-nondet-stimcomm} states that when non-determinism is added at the sink of a 
potential communication path via stimuli, the potential for communication is preserved only if there does not exist any basic stimulus that is 
generated by the source that influences agent~$\Agent{B}$ and agent~$\Agent{C}$ to behave as a sub-behaviour of agent~$\Agent{B + C}$. This 
condition ensures that agent~$\Agent{B + C}$ cannot have a fixed point behaviour.
›

lemma source_nondet_stimcomm: "(B 𝒮 C)  ((A + B) 𝒮 C)"
proof -
  assume "B 𝒮 C"
  then obtain s t where st: "s  𝒮a  t  𝒮a  t 𝒮 λ(s,B)  t  C  C" 
    by (auto simp only: dcs_def)
  show "(A + B) 𝒮 C"
    unfolding dcs_def 
    by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto simp add: st inf_add_S_left)
qed

lemma comm_source_nondet_stimcomm: "(B 𝒮 C)  ((B + A) 𝒮 C)"
  by (simp add: source_nondet_stimcomm algebra_simps)

lemma sink_sum_stimcomm: "( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C))  (A 𝒮 B + C)"
proof -
  assume " s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C)"
  then obtain s t where st: "s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C)" by auto
  have "t  (B + C) = B + C  False"
  proof -
    assume fixbc: "t  (B + C) = B + C"
    have "t  B  𝒦 t  (B + C)"
      by (simp, rule inf_add_K_right)
    moreover have "t  C  𝒦 t  (B + C)"
      by (simp, rule inf_add_K_left)
    ultimately have "t  B 𝒦 B + C  t  C 𝒦 B + C" 
      by (simp only: fixbc)
    thus False by (simp only: st) 
  qed
  thus "A 𝒮 B + C"
    unfolding dcs_def
    by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto simp only: st)
qed

lemma sink_nondet_stimcomm: "A 𝒮 B  ( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A) 
 ¬(t  B 𝒦 B + C  t  C 𝒦 B + C))  (A 𝒮 B + C)"
proof (rule sink_sum_stimcomm)
  assume h1: "A 𝒮 B"
  assume h2: "( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C))"
  show " s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C)"
  proof -
    from h1 obtain s t where "s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  t  B  B"
      by (auto simp only: dcs_def)
    from this h2 have "s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  
¬(t  B 𝒦 B + C  t  C 𝒦 B + C)" by auto
    thus ?thesis
      by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto)
  qed
qed

subsubsection ‹Potential for Communication via Shared Environments \label{ssub:pfc_env}›

text ‹
Lemmas \emph{source-nondet-envcomm} and \emph{sink-nondet-envcomm} show how the potential for communication via shared environments is preserved when non-determinism is 
introduced at the source or the sink of a potential communication path via shared environments.
›

lemma source_nondet_envcomm: "B  C  (A + B)  C"
  by (simp add: sum_dce)

lemma sink_nondet_envcomm: "A  B  A  (B + C)"
  by (simp add: dce_sum)

 
subsection ‹Preserving the Potential for Communication with Agent Behaviour Modifications\label{sub:preservation}›

text ‹
The following results identify the conditions constraining the modifications that can be made to the source or sink agent involved in a direct potential for communication to 
preserve the communication in a distributed system. In this way, it demonstrates the conditions under which a modification to an agent behaviour can be made while maintaining 
the communicating behaviour of the agents in the system.

Specifically, Lemma \emph{sink-seq-stimcomm} shows how the sequential composition of an additional behaviour on the left of a sink agent will not affect the potential for communication 
provided that every stimulus that is generated by the source agent either does not fix the behaviour of the first component of the sequential composition, or causes the 
first component of the sequential composition to generate a stimulus that does not fix the behaviour of the second component of the sequential composition. Alternatively, 
Lemma \emph{nondet-right-source-communication} shows how non-determinism added on the right of a source agent will not affect the potential for communication provided that 
the non-deterministic behaviours can be influenced by the source agent to stop being a sub-behaviour of the non-deterministic behaviour.
›


lemma sink_seq_stimcomm: "A 𝒮 B 
  s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  λ(t,C) = t  A;C 𝒮 B"
proof -
  assume "A 𝒮 B"
  then obtain s t where st: "s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  t  B  B" 
    unfolding dcs_def by auto
  assume " s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A)  λ(t,C) = t"
  from this st have tfix: "λ(t,C) = t" by auto
  have "λ(t,C) 𝒮  λ(λ(s,A),C)" by (simp add: inf_S_next_stimulus st)
  hence "t 𝒮 λ (λ (s, A), C)" by (simp add: tfix)
  thus "A;C 𝒮 B" 
    unfolding dcs_def
    by (rule_tac x="s" in exI, rule_tac x="t" in exI, simp add: st)
qed

lemma nondet_right_source_communication: "A  C  C  B  ( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A) 
 ¬(t  C 𝒦 C + D  t  D 𝒦 C + D))  A  C+D  C+D  B"
proof -
  assume h1:"A  C  C  B"
  assume h2:"( s t. s  𝒮a  t  𝒮a  t 𝒮 λ(s,A) 
 ¬(t  C 𝒦 C + D  t  D 𝒦 C + D))"
  from h2 have hs: "A 𝒮 C  A 𝒮 C+D" 
    by (auto simp add: sink_nondet_stimcomm)
  have "A  C  A  C+D"
    unfolding pdc_def
    using dce_sum hs by blast
  moreover have "C  B  C + D  B"
    unfolding pdc_def
    using comm_source_nondet_stimcomm sum_dce by blast
  ultimately show "A  C+D  C+D  B"
    by (simp add: h1)
qed

end

end