Theory C2KA
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" and "Jaskolka2013aa" and "Jaskolka2014aa"›.
›
theory C2KA
imports CKA Stimuli
begin
no_notation comp (infixl ‹∘› 55)
unbundle no rtrancl_syntax
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, t∘a) ⊙ λ(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) ⊕ λ(s⊕t,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) = λ(s⊕t,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