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