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