Theory FLPExistingSystem

section ‹An Existing FLPSystem›

theory FLPExistingSystem
imports FLPTheorem
begin

text ‹
  We define an example FLPSystem with some example execution to show that the
  locales employed are not void. (If they were, the consensus impossibility
  result would be trivial.)
›

subsection ‹System definition›

datatype proc = p0 | p1
datatype state = s0 | s1
datatype val = v0 | v1

primrec trans :: "proc ⇒ state ⇒ val messageValue ⇒ state"
where
  "trans p s0 v = s1"
| "trans p s1 v = s0"

primrec sends ::
  "proc ⇒ state ⇒ val messageValue ⇒ (proc, val) message multiset"
where
  "sends p s0 v = {# <p0, v1> }"
| "sends p s1 v = {# <p1, v0> }"

definition start :: "proc ⇒ state"
where "start p  ≡ s0"

― ‹An example execution›
definition exec ::
  "(proc, val, state ) configuration list"
where
  exec_def: "exec ≡ [ ⦇ 
    states = (λp. s0),
    msgs = ({# <p0, inM True> } ∪# {# <p1, inM True> }) ⦈ ]"

lemma ProcUniv: "(UNIV :: proc set) = {p0, p1}"
  by (metis UNIV_eq_I insert_iff proc.exhaust)

subsection ‹Interpretation as FLP Locale›

interpretation FLPSys: flpSystem trans sends start
proof
  ― ‹finiteProcs›
  show "finite (UNIV :: proc set)"
    unfolding ProcUniv by simp
next
  ― ‹minimalProcs›
  have "card (UNIV :: proc set) = 2"
    unfolding ProcUniv by simp
  thus "2 ≤ card (UNIV :: proc set)" by simp
next
  ― ‹finiteSends›
  fix p s m
  have FinExplSends: "finite {<p0, v1>, <p1, v0>}" by auto
  have "{v. 0 < sends p s m v} ⊆ {<p0, v1>, <p1, v0>}"
  proof auto
    fix x
    assume "x ≠ <p0, v1>" "0 < sends p s m x"
    thus "x = <p1, v0>"
      by (metis (full_types) neq0_conv sends.simps(1,2) state.exhaust)
  qed
  thus "finite {v. 0 < sends p s m v}"
    using FinExplSends finite_subset by blast
next
  ― ‹noInSends›
  fix p s m p2 v
  show "sends p s m <p2, inM v> = 0" by (induct s, auto)
qed

interpretation FLPExec: execution trans sends start exec "[]"
proof
  ― ‹notEmpty›
  show "1 ≤ length exec"
    by (simp add:exec_def)
next
  ― ‹length›
  show "length exec - 1 = length []"
    by (simp add:exec_def)
next
  ― ‹base›
  show "asynchronousSystem.initial start (hd exec)"
    unfolding asynchronousSystem.initial_def isReceiverOf_def
    by (auto simp add: start_def exec_def, metis proc.exhaust)
next
  ― ‹step›
  fix i cfg1 cfg2
  assume "i < length exec - 1"
  hence "False" by (simp add:exec_def)
  thus "asynchronousSystem.steps FLPExistingSystem.trans sends cfg1 ([] ! i) cfg2"
    by rule
qed

end