Theory FLPSystem

section‹FLPSystem›

text ‹
  \file{FLPSystem} extends \file{AsynchronousSystem} with concepts of consensus
  and decisions. It develops a concept of non-uniformity regarding pending
  decision possibilities, where non-uniform configurations can always
  reach other non-uniform ones.
›

theory FLPSystem
imports AsynchronousSystem ListUtilities
begin

subsection‹Locale for the FLP consensus setting›

locale flpSystem =
  asynchronousSystem trans sends start    
    for trans :: "'p  's  'v messageValue 's"
    and sends :: "'p  's  'v messageValue  ('p, 'v) message multiset"
    and start :: "'p  's" +
assumes finiteProcs: "finite Proc"
    and minimalProcs: "card Proc  2"
    and finiteSends: "finite {v. v ∈# (sends p s m)}"
    and noInSends: "sends p s m <p2, inM v> = 0"
begin

subsection‹Decidedness and uniformity of configurations›

abbreviation vDecided ::
  "bool  ('p, 'v, 's) configuration  bool"
where
  "vDecided v cfg  initReachable cfg  (<⊥, outM v> ∈# msgs cfg)"

abbreviation decided ::
  "('p, 'v, 's) configuration  bool"
where
  "decided cfg  (v . vDecided v cfg)"

definition pSilDecVal ::
  "bool  'p  ('p, 'v, 's) configuration  bool"
where
  "pSilDecVal v p c  initReachable c  
    ( c'::('p, 'v, 's) configuration . (withoutQReachable c {p} c') 
     vDecided v c')"

abbreviation pSilentDecisionValues ::
  "'p  ('p, 'v, 's) configuration  bool set" ("val[_,_]")
where 
  "val[p, c]  {v. pSilDecVal v p c}"

definition vUniform ::
  "bool  ('p, 'v, 's) configuration  bool"
where 
  "vUniform v c  initReachable c  (p. val[p,c] = {v})"

abbreviation nonUniform ::
  "('p, 'v, 's) configuration  bool"
where
  "nonUniform c  initReachable c 
    ¬(vUniform False c)  
    ¬(vUniform True c)"

subsection‹Agreement, validity, termination›

text‹
  Völzer defines consensus in terms of the classical notions
  of agreement, validity, and termination. The proof then mostly applies a
  weakened notion of termination, which we refer to as ,,pseudo termination''.
›

definition agreement ::
  "('p, 'v, 's) configuration  bool"
where 
  "agreement c  
    (v1. (<⊥, outM v1> ∈# msgs c) 
       (v2. (<⊥, outM v2> ∈# msgs c) 
         v2 = v1))"

definition agreementInit ::
  "('p, 'v, 's) configuration  ('p, 'v, 's) configuration  bool"
where 
  "agreementInit i c  
    initial i  reachable i c  
      (v1. (<⊥, outM v1> ∈# msgs c) 
         (v2. (<⊥, outM v2> ∈# msgs c) 
           v2 = v1))"

definition validity ::
  "('p, 'v, 's) configuration  ('p, 'v, 's) configuration  bool"
where
  "validity i c 
    initial i  reachable i c  
      (v. (<⊥, outM v> ∈# msgs c) 
         (p. (<p, inM v> ∈# msgs i)))"

text‹
  The termination concept which is implied by the concept of "pseudo-consensus"
  in the paper.
›
definition terminationPseudo ::
  "nat  ('p, 'v, 's) configuration  'p set  bool"
where
  "terminationPseudo t c Q  ((initReachable c  card Q + t  card Proc) 
     (c'. qReachable c Q c'  decided c'))"

subsection ‹Propositions about decisions›

text‹
  For every process \var{p} and every configuration that is reachable from an
  initial configuration (i.e. \isb{initReachable} \var{c}) we have
  $\var{val(p,c)} \neq \emptyset$.

  This follows directly from the definition of \var{val} and the definition of
  \isb{terminationPseudo}, which has to be assumed to ensure that there is a
  reachable configuration that is decided.
  
  \voelzer{Proposition 2(a)}
›
lemma DecisionValuesExist:
fixes
  c :: "('p, 'v, 's) configuration" and
  p :: "'p" 
assumes
  Termination: "cc Q . terminationPseudo 1 cc Q" and
  Reachable: "initReachable c"      
shows
  "val[p,c]  {}"  
proof -
  from Termination
    have "(initReachable c  card Proc  card (UNIV - {p}) + 1) 
       (c'. qReachable c (UNIV-{p}) c'  initReachable c' 
       (v. 0 < msgs c' <⊥, outM v>))"
    unfolding terminationPseudo_def by simp
  with Reachable minimalProcs finiteProcs
    have "c'. qReachable c (UNIV - {p}) c'  initReachable c' 
     (v. 0 < msgs c' <⊥, outM v>)"
    unfolding terminationPseudo_def initReachable_def by simp
  thus ?thesis
    unfolding pSilDecVal_def 
    using Reachable by auto
qed

text‹
  The lemma \isb{DecidedImpliesUniform} proves that every \isb{vDecided}
  configuration \var{c} is also \isb{vUniform}. Völzer claims that this
  follows directly from the definitions of \isb{vDecided} and \isb{vUniform}.
  But this is not quite enough: One must also assume \isb{terminationPseudo}
  and \isb{agreement} for all reachable configurations.

  \voelzer{Proposition 2(b)}
›
lemma DecidedImpliesUniform:
fixes
  c :: "('p, 'v, 's) configuration" and
  v :: "bool"
assumes
  AllAgree: " cfg . reachable c cfg  agreement cfg" and
  Termination: "cc Q . terminationPseudo 1 cc Q" and
  VDec: "vDecided v c"
shows
  "vUniform v c"
  using AllAgree VDec unfolding agreement_def vUniform_def pSilDecVal_def 
proof simp 
  assume 
    Agree: "cfg. reachable c cfg 
      (v1. 0 < msgs cfg <⊥, outM v1> 
       (v2. (0 < msgs cfg <⊥, outM v2>) = (v2 = v1)))" and 
    vDec: "initReachable c  0 < msgs c <⊥, outM v>"
  show 
    "(p. {v. c'. qReachable c (Proc - {p}) c'  initReachable c'  
      0 < msgs c' <⊥, outM v>} = {v})" 
  proof clarify
    fix p 
    have "val[p,c]  {}" using Termination DecisionValuesExist vDec 
      by simp
    hence NotEmpty: "{v. c'. qReachable c (UNIV - {p}) c' 
       initReachable c'  0 < msgs c' <⊥, outM v>}  {}" 
      using pSilDecVal_def by simp
    have U: " u . u  {v. c'. qReachable c (UNIV - {p}) c' 
       initReachable c'  0 < msgs c' <⊥, outM v>}  (u = v)" 
    proof clarify
      fix u c'
      assume "qReachable c (UNIV - {p}) c'" "initReachable c'"
      hence Reach: "reachable c c'" using QReachImplReach by simp
      from VDec have Msg: "0 < msgs c <⊥, outM v>" by simp
      from Reach NoOutMessageLoss have 
        "msgs c <⊥, outM v>  msgs c' <⊥, outM v>" by simp
      with Msg have VMsg: "0 < msgs c' <⊥, outM v>" 
        using NoOutMessageLoss Reach by (metis less_le_trans)
      assume "0 < msgs c' <⊥, outM u>"
      with Agree VMsg Reach show "u = v" by simp
    qed
    thus " {v. c'. qReachable c (UNIV - {p}) c'  initReachable c'  
      0 < msgs c' <⊥, outM v>} = {v}" using NotEmpty U by auto  
  qed
qed

corollary NonUniformImpliesNotDecided:
fixes
  c :: "('p, 'v, 's) configuration" and
  v :: "bool"
assumes
  " cfg . reachable c cfg  agreement cfg"
  "cc Q . terminationPseudo 1 cc Q"
  "nonUniform c"
  "vDecided v c"
shows
  "False"
using DecidedImpliesUniform[OF assms(1,2,4)] assms(3)
  by (cases v, simp_all)
      
text‹
  All three parts of Völzer's Proposition 3 consider a single step from an
  arbitrary \isb{initReachable} configuration \var{c} with a message
  $\var{msg}$ to a succeeding configuration \var{c'}.
›

text‹
  The silent decision values of a process which is not active in a step only
  decrease or stay the same.
  
  This follows directly from the definitions and the transitivity of the
  reachability properties \isb{reachable} and \isb{qReachable}.

  \voelzer{Proposition 3(a)}
›
lemma InactiveProcessSilentDecisionValuesDecrease:
fixes 
  p q :: 'p and
  c c' :: "('p, 'v, 's) configuration" and
  msg :: "('p, 'v) message"
assumes 
  "p  q" and
  "c  msg  c'" and
  "isReceiverOf p msg" and
  "initReachable c"
shows 
  "val[q,c']  val[q,c]"
proof(auto simp add: pSilDecVal_def assms(4))
  fix x cfg'
  assume 
    Msg: "0 < msgs cfg' <⊥, outM x>" and 
    Cfg': "qReachable c' (Proc - {q}) cfg'"
  have "initReachable c'"
    using assms initReachable_def reachable.simps 
    by blast
  hence Init: "initReachable cfg'" 
    using Cfg' initReachable_def QReachImplReach[of c' "(Proc - {q})" cfg'] 
    ReachableTrans by blast
  have "p  Proc - {q}"
    using assms by blast
  hence "qReachable c (Proc - {q}) c'"
    using assms qReachable.simps by metis
  hence "qReachable c (Proc - {q}) cfg'"
    using Cfg' QReachableTrans
    by blast
  with Msg Init show 
    "c'a. qReachable c (Proc - {q}) c'a 
       initReachable c'a  
      0 < msgs c'a <⊥, outM x>" by blast
qed

text‹
  ...while the silent decision values of the process which is active in
  a step may only increase or stay the same.
  
  This follows as stated in cite"Voelzer" from the \emph{diamond property}
  for a reachable configuration and a single step, i.e. \isb{DiamondTwo},
  and in addition from the fact that output messages cannot get lost, i.e.
  \isb{NoOutMessageLoss}.

  \voelzer{Proposition 3(b)}
›
lemma ActiveProcessSilentDecisionValuesIncrease :
fixes 
  p q :: 'p and
  c c' :: "('p, 'v, 's) configuration" and
  msg :: "('p, 'v) message"
assumes 
  "p = q" and
  "c  msg  c'" and
  "isReceiverOf p msg" and
  "initReachable c"
shows "val[q,c]  val[q,c']"
proof (auto simp add: pSilDecVal_def assms(4))
  from assms initReachable_def reachable.simps show "initReachable c'" 
    by meson
  fix x cv 
  assume Cv: "qReachable c (Proc - {q}) cv" "initReachable cv" 
    "0 < msgs cv <⊥, outM x>" 
  have "c'a. (cv  msg  c'a)  qReachable c' (Proc - {q}) c'a" 
    using DiamondTwo Cv(1) assms 
    by blast
  then obtain c'' where C'': "(cv  msg  c'')" 
    "qReachable c' (Proc - {q}) c''" by auto
  with Cv(2) initReachable_def reachable.simps
    have Init: "initReachable c''" by blast
  have "reachable cv c''" using C''(1) reachable.intros by blast      
  hence "msgs cv <⊥, outM x>  msgs c'' <⊥, outM x>" using NoOutMessageLoss 
    by simp
  hence "0 < msgs c'' <⊥, outM x>" using Cv(3) by auto
  thus "c'a. qReachable c' (Proc - {q}) c'a  
     initReachable c'a  0 < msgs c'a <⊥, outM x>" 
    using C''(2) Init by blast
qed

text‹
  As a result from the previous two propositions, the silent decision values
  of a process cannot go from {0} to {1} or vice versa in a step.

  This is a slightly more generic version of Proposition 3 (c) from
  cite"Voelzer" since it is proven for both values, while Völzer is only
  interested in the situation starting with $\var{val(q,c) = \{0\}}$.

  \voelzer{Proposition 3(c)}
›
lemma SilentDecisionValueNotInverting:
fixes 
  p q :: 'p and
  c c' :: "('p, 'v, 's) configuration" and
  msg :: "('p, 'v) message" and
  v :: bool
assumes 
  Val: "val[q,c] = {v}" and
  Step:  "c  msg  c'" and
  Rec:  "isReceiverOf p msg" and
  Init: "initReachable c"
shows 
  "val[q,c']  {¬ v}"
proof(cases "p = q")
  case False
    hence "val[q,c']  val[q,c]"
      using Step Rec InactiveProcessSilentDecisionValuesDecrease Init by simp
    with Val show "val[q,c']  {¬ v}" by auto
  next
  case True
    hence "val[q,c]  val[q,c']"
      using Step Rec ActiveProcessSilentDecisionValuesIncrease Init by simp
    with Val show "val[q,c']  {¬ v}" by auto
qed

subsection‹Towards a proof of FLP›

text‹
  There is an \isb{initial} configuration that is \isb{nonUniform} under
  the assumption of \isb{validity}, \isb{agreement} and \isb{terminationPseudo}.

  The lemma is used in the proof of the main theorem to construct the
  \isb{non\-Uni\-form} and \isb{initial} configuration that leads to the
  final contradiction.

  \voelzer{Lemma 1}
›
lemma InitialNonUniformCfg:
assumes
  Termination: "cc Q . terminationPseudo 1 cc Q" and
  Validity: " i c . validity i c" and
  Agreement: " i c . agreementInit i c"
shows 
  " cfg . initial cfg  nonUniform cfg" 
proof-
  obtain n::nat where N: "n = card Proc" by blast
  hence " procList::('p list). length procList = n  set procList = Proc 
     distinct procList" 
    using finiteProcs 
    by (metis distinct_card finite_distinct_list)  
  then obtain procList where 
    ProcList: "length procList = n" "set procList = Proc" 
      "distinct procList" by blast
  have AllPInProclist: "p. i<n. procList ! i = p"
    using ProcList N 
  proof auto
    fix p
    assume Asm: "set procList = Proc" "length procList = card Proc"
    have "p  set procList" using ProcList by auto
    with Asm in_set_conv_nth
      show "i<card Proc. procList ! i = p" by metis
  qed
  have NGr0: "n > 0"
    using N finiteProcs minimalProcs by auto
  define initMsg :: "nat  ('p, 'v) message  nat"
    where "initMsg ind m = (if p. m = <p, inM (i<ind. procList!i = p)> then 1 else 0)" for ind m
  define initCfgList
    where "initCfgList = map (λind. states = start, msgs = initMsg ind) [0..<(n+1)]"
  have InitCfgLength: "length initCfgList = n + 1" 
    unfolding initCfgList_def by auto
  have InitCfgNonEmpty: "initCfgList  []"  
    unfolding initCfgList_def by auto
  hence InitCfgStart: "(c  set initCfgList. states c = start)" 
    unfolding initCfgList_def by auto
  have InitCfgSet: "set initCfgList = 
    {x. ind < n+1. x = states = start, msgs = initMsg ind}"
    unfolding initCfgList_def
  proof auto
    fix ind
    assume "ind < n"
    hence "inda<Suc n. inda = ind  initMsg ind = initMsg inda" by auto
    thus "inda<Suc n. initMsg ind = initMsg inda" by blast
  next
    fix ind
    assume Asm:
      "states = start, msgs = initMsg ind  (λind::nat. states = start, msgs = initMsg ind) ` {0..<n}"
      "ind < Suc n"
    hence "ind  n" by auto
    with Asm have "ind = n" by auto
    thus "initMsg ind = initMsg n" by auto
  qed
  have InitInitial: "c  set initCfgList . initial c"
    unfolding initial_def initCfgList_def initMsg_def using InitCfgStart
    by auto
  with InitCfgSet have InitInitReachable: 
    " c  set initCfgList . initReachable c"
    using reachable.simps
    unfolding initReachable_def
    by blast

  define c0 where "c0 = initCfgList ! 0"
  hence "c0 =  states = start, msgs = initMsg 0 "
    using InitCfgLength nth_map_upt[of 0 "n+1" 0]
    unfolding initCfgList_def by auto
  hence MsgC0: "msgs c0 = (λm. if p. m = <p, inM False> then 1 else 0)"
    unfolding initMsg_def by simp
      
  define cN where "cN = initCfgList ! n"
  hence "cN =  states = start, msgs = initMsg n"
    using InitCfgLength nth_map_upt[of n "n+1" 0]
    unfolding initCfgList_def
    by auto
  hence MsgCN: "msgs cN = (λm. if p. m = <p, inM True> then 1 else 0)"
    unfolding initMsg_def
    using AllPInProclist
    by auto

  have C0NotCN: "c0  cN"
  proof
    assume "c0 = cN"
    hence StrangeEq: "(λm::('p, 'v) message.
        if p. m = <p, inM False> then 1 else 0 :: nat) =
      (λm. if p. m = <p, inM True> then 1 else 0)"
      using InitCfgLength N minimalProcs MsgC0 MsgCN 
      unfolding c0_def cN_def by auto
    thus "False"
      by (metis message.inject(1) zero_neq_one)
  qed

  have C0NAreUniform: " cX . (cX = c0)  (cX = cN) 
                       vUniform (cX = cN) cX" 
  proof-
    fix cX
    assume xIs0OrN: "(cX = c0)  (cX = cN)"
    have xInit: "initial cX"
      using InitCfgLength InitCfgSet set_conv_nth[of initCfgList] xIs0OrN
      unfolding c0_def cN_def
      by (auto simp add: InitInitial)
    from Validity
      have COnlyReachesOneDecision:
        " c . reachable cX c  decided c  (vDecided (cX = cN) c)"
      unfolding validity_def initReachable_def
    proof auto
      fix c cfg0 v
      assume
        Validity: "(i c. ((initial i)  (reachable i c)) 
          (v. (0 < msgs c (<⊥, outM v>)) 
           (p. (0 < msgs i (<p, inM v>)))))" and
        OutMsg: "0 < msgs c <⊥, outM v>" and
        InitCXReachable: "reachable cX c"
      thus "0 < msgs c <⊥, outM (cX = cN)>"
        using xIs0OrN 
      proof (cases "v = (cX = cN)", simp)
        assume "v  (cX = cN)"
        hence vDef: "v = (cX  cN)" by auto
        with Validity InitCXReachable OutMsg xInit
          have ExistMsg: "p. (0 < msgs cX (<p, inM (cX  cN)>))" by auto
        with initMsg_def have False
          using xIs0OrN
          by (auto simp add: MsgC0 MsgCN C0NotCN) 
        thus "0 < msgs c <⊥, outM cX = cN>" by simp
      qed
    qed
    have InitRInitC: "initReachable cX" using xInit InitialIsInitReachable 
      by auto
    have NoWrongDecs: " v p cc::('p, 'v, 's) configuration.
      qReachable cX (Proc - {p}) cc  initReachable cc 
       0 < msgs cc <⊥, outM v> 
         v = (cX = cN)"
    proof clarify
      fix v p cc
      assume Asm: "qReachable cX (Proc - {p}) cc" "initReachable cc" 
      "0 < msgs cc <⊥, outM v>"
      hence "reachable cX cc" "decided cc" using QReachImplReach by auto
      hence "¬(vDecided (cX  cN) cc)"
        using COnlyReachesOneDecision Agreement Asm C0NotCN xInit xIs0OrN
        unfolding agreementInit_def by metis
      with Asm C0NotCN xIs0OrN show "v = (cX = cN)" 
      by (auto, metis (full_types) neq0_conv)
    qed
    have ExRightDecs: "p. cc. qReachable (cX) (Proc - {p}) cc
       initReachable cc  0 < msgs cc <⊥, outM (cX = cN)>"
    proof-
      fix p
      show "cc::('p, 'v, 's) configuration.
           qReachable cX (Proc - {p}) cc  initReachable cc 
            (0::nat) < msgs cc <⊥, outM cX = cN>"
        using Termination[of "cX" "Proc - {p}"] finiteProcs minimalProcs 
          InitRInitC
        unfolding terminationPseudo_def
      proof auto
        fix cc v
        assume 
          Asm: "initReachable cX" "qReachable (cX) (Proc - {p}) cc"
          "initReachable cc"  "0 < msgs cc <⊥, outM v>"
        with COnlyReachesOneDecision[rule_format, of "cc"] QReachImplReach
          have "0 < msgs cc <⊥, outM cX = cN>" by auto
        with Asm
          show "cc::('p, 'v, 's) configuration. 
            qReachable cX (Proc - {p}) cc
             initReachable cc  (0::nat) < msgs cc <⊥, outM cX = cN>" 
            by blast
      qed
    qed
    have ZeroinPSilent: " p v . v  val[p, cX]  v = (cX = cN)"
    proof clarify
      fix p v
      show "v  val[p, cX]  v = (cX = cN)"
        unfolding pSilDecVal_def
        using InitRInitC xIs0OrN C0NotCN NoWrongDecs ExRightDecs by auto
    qed
    thus "vUniform (cX = cN) cX" using InitRInitC 
      unfolding vUniform_def by auto
  qed
  hence
    C0Is0Uniform: "vUniform False c0" and
    CNNot0Uniform: "¬ vUniform False cN"
    using C0NAreUniform unfolding vUniform_def using C0NotCN by auto
  hence " j < n. vUniform False (initCfgList ! j) 
     ¬(vUniform False (initCfgList ! Suc j))"
    unfolding c0_def cN_def
    using NatPredicateTippingPoint
      [of n "λx. vUniform False (initCfgList ! x)"] NGr0 by auto
  then obtain j
    where J: "j < n"
      "vUniform False (initCfgList ! j)"
      "¬(vUniform False (initCfgList ! Suc j))" by blast
  define pJ where "pJ = procList ! j"
  define cJ where "cJ = initCfgList ! j"
  hence cJDef: "cJ =  states = start, msgs = initMsg j"
    using J(1) InitCfgLength nth_map_upt[of 0 "j- 1" 1] 
      nth_map_upt[of "j" "n + 1" 0]
    unfolding initCfgList_def 
    by auto
  hence MsgCJ: "msgs cJ = (λm::('p, 'v) message.
    if p::'p. m = <p, inM i<j. procList ! i = p> then 1::nat
    else (0::nat))"
    unfolding initMsg_def
    using AllPInProclist
    by auto
  define cJ1 where "cJ1 = initCfgList ! (Suc j)"
  hence cJ1Def: "cJ1 =  states = start, msgs = initMsg (Suc j)"
    using J(1) InitCfgLength nth_map_upt[of 0 "j" 1] 
    nth_map_upt[of "j + 1" "n + 1" 0]
    unfolding initCfgList_def 
    by auto
  hence MsgCJ1: "msgs cJ1 = (λm::('p, 'v) message.
    if p::'p. m = <p, inM i<(Suc j). procList ! i = p> then 1::nat
    else (0::nat))"
    unfolding initMsg_def
    using AllPInProclist
    by auto
  have CJ1Init: "initial cJ1"
    using InitInitial[rule_format, of cJ1]  J(1) InitCfgLength 
    unfolding cJ1_def by auto
  hence CJ1InitR: "initReachable cJ1"
    using InitialIsInitReachable by simp
  have ValPj0: "False  val[pJ, cJ]"
    using J(2) unfolding cJ_def vUniform_def by auto
  hence "cc. vDecided False cc  withoutQReachable cJ {pJ} cc"
    unfolding pSilDecVal_def by auto
  then obtain cc
    where CC: "vDecided False cc" "withoutQReachable cJ {pJ} cc"
    by blast
    hence "Q. qReachable cJ Q cc  Q = Proc - {pJ}" by blast
    then obtain ccQ where CCQ: "qReachable cJ ccQ cc" "ccQ = Proc - {pJ}" 
      by blast
  have StatescJcJ1: "states cJ = states cJ1" 
    using  cJ_def cJ1_def initCfgList_def  
    by (metis InitCfgLength InitCfgStart J(1) Suc_eq_plus1 Suc_mono 
      less_SucI nth_mem) 
  have Distinct: " i . distinct procList  i<j 
     procList ! i = procList ! j  False"
    by (metis J(1) ProcList(1) distinct_conv_nth less_trans 
       not_less_iff_gr_or_eq)
  have A: "msgs cJ (<pJ ,inM False>) = 1" 
    using pJ_def ProcList J(1) MsgCJ using Distinct by auto
  have B: "msgs cJ1 (<pJ ,inM True>) = 1" 
    using pJ_def ProcList J(1) MsgCJ1 by auto
  have C: "msgs cJ (<pJ ,inM True>) = 0" 
    using pJ_def ProcList J(1) MsgCJ using Distinct by auto  
  have D: "msgs cJ1 (<pJ ,inM False>) = 0" 
    using pJ_def ProcList J(1) MsgCJ1 by auto
  define msgsCJ' where
    "msgsCJ' m = (if m = (<pJ ,inM False>)  m = (<pJ ,inM True>) then 0 else (msgs cJ) m)" for m
  have MsgsCJ': "msgsCJ' = ((msgs cJ) -# (<pJ ,inM False>))"
    using A C msgsCJ'_def by auto
  have AllOther: " m . msgsCJ' m = ((msgs cJ1) -# (<pJ ,inM True>)) m"
    using B D MsgCJ1 MsgCJ  J(1) N ProcList AllPInProclist 
    unfolding msgsCJ'_def pJ_def
  proof(clarify)
    fix m
    show "(if m = <procList ! j, inM False>  
        m = <procList ! j, inM True> then 0 else msgs cJ m) 
      = (msgs cJ1 -# <procList ! j, inM True>) m"
    proof(cases "m = <procList ! j, inM False>  m 
      = <procList ! j, inM True>",auto)
      assume "0 < (msgs cJ1 <procList ! j, inM False>)"
      thus False using D pJ_def by (metis less_nat_zero_code)
    next
      show "msgs cJ1 <procList ! j, inM True>  Suc 0" 
        by (metis B One_nat_def order_refl pJ_def)
    next
      assume AssumpMJ: "m  <procList ! j, inM False>" 
                       "m  <procList ! j, inM True>"
      hence "(if p. m = <p, inM i<j. procList ! i = p> then 1 else 0)
           = (if p. m = <p, inM i<Suc j. procList ! i = p> then 1 else 0)"
        by (induct m, auto simp add: less_Suc_eq)
      thus "msgs cJ m = msgs cJ1 m"
        using MsgCJ MsgCJ1 by auto
    qed
  qed ― ‹of AllOther›

  with MsgsCJ' have InitMsgs: "((msgs cJ) -# (<pJ ,inM False>)) 
    = ((msgs cJ1) -# (<pJ, inM True>))"
    by simp 
  hence F: "(((msgs cJ) -# (<pJ ,inM False>)) ∪# ({#<pJ, inM True>})) =
    (((msgs cJ1) -# (<pJ, inM True>))  ∪# ({#<pJ, inM True>}))" 
    by (metis (full_types))
  from B have One: "(((msgs cJ1) -# (<pJ, inM True>)) 
    ∪# ({#<pJ, inM True>})) <pJ, inM True> = 1" by simp
  with B have " m :: ('p, 'v) message . (msgs cJ1) m 
    = (((msgs cJ1) -# (<pJ, inM True>))  ∪# 
    ({#<pJ, inM True>})) m" by simp
  with B have "(((msgs cJ1) -# (<pJ, inM True>))  ∪# ({#<pJ, inM True>})) 
    = (msgs cJ1)" by simp
  with F have InitMsgs: "(((msgs cJ) -# (<pJ ,inM False>)) 
    ∪# ({#<pJ, inM True>})) = (msgs cJ1)" 
    by simp
  define cc' where "cc' = states = (states cc),
    msgs = (((msgs cc) -# (<pJ,inM False>)) ∪# {# (<pJ, inM True>)})"
  have "qReachable cJ ccQ cc; ccQ = Proc - {pJ}; 
    (((msgs cJ) -# (<pJ ,inM False>)) ∪# ({#<pJ, inM True>})) 
      = (msgs cJ1); states cJ = states cJ1 
       withoutQReachable cJ1 {pJ} states = (states cc), 
      msgs = (((msgs cc) -# (<pJ,inM False>)) ∪# {# (<pJ, inM True>)}) "
    proof (induct rule: qReachable.induct)
      fix cfg1::"('p, 'v, 's) configuration" 
      fix Q
      assume 
        Assm: "(((msgs cfg1) -#(<pJ, inM False>)) ∪# {# <pJ, inM True> })
        = msgs cJ1" 
        "states cfg1 = states cJ1"
      hence CJ1: "cJ1 = states = states cfg1, 
        msgs = ((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> }" by auto
      have "qReachable cJ1  (Proc - {pJ}) cJ1" using qReachable.simps 
        by blast
      with Assm show "qReachable cJ1 (Proc - {pJ})
        states = states cfg1, msgs = ((msgs cfg1) -# <pJ, inM False>) 
        ∪# {# <pJ, inM True> }" using CJ1 by blast
      fix cfg1 cfg2 cfg3 :: "('p, 'v, 's) configuration"
      fix msg
      assume Q: "Q = (Proc - {pJ})"
      assume "(((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> }) 
        = (msgs cJ1)"
        "(states cfg1) = (states cJ1)"
        "Q = (Proc - {pJ}) 
          (((msgs cfg1) -# <pJ, inM False>) ∪# {# <pJ, inM True> }) 
            = (msgs cJ1) 
           (states cfg1) = (states cJ1) 
           qReachable cJ1 (Proc - {pJ})
          states = (states cfg2),
          msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })"
      with Q have Cfg2: 
        "qReachable cJ1 (Proc - {pJ}) states = (states cfg2),
        msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })" 
        by simp
      assume "qReachable cfg1 Q cfg2" 
        "cfg2  msg  cfg3"
        "(p::'p)Q. (isReceiverOf p msg)"
      with Q have Step: "qReachable cfg1 (Proc - {pJ}) cfg2" 
        "cfg2  msg  cfg3"
        "(p::'p)(Proc - {pJ}). (isReceiverOf p msg)" by auto
      then obtain p where P: "p(Proc - {pJ})" "isReceiverOf p msg" by blast
      hence NotEq: "pJ  p" by blast
      with UniqueReceiverOf[of "p" "msg" "pJ"] P(2) 
        have notRec: "¬ (isReceiverOf pJ msg)" by blast
      hence MsgNoIn:"msg   <pJ, inM False>  msg   <pJ, inM True>" 
        by auto 
      from Step(2) have "enabled cfg2 msg" using steps.simps 
        by (auto, cases msg, auto)
      hence MsgEnabled: "enabled states = (states cfg2),
        msgs = (((msgs cfg2) -# <pJ, inM False>) 
        ∪# {# <pJ, inM True> }) msg" 
        using MsgNoIn by (simp add: enabled_def)
      have  "states = (states cfg2),
              msgs = (((msgs cfg2) -# <pJ, inM False>) 
              ∪# {# <pJ, inM True> })
                 msg  states = (states cfg3),
                msgs = (((msgs cfg3) -# <pJ, inM False>) 
                ∪# {# <pJ, inM True> })" 
      proof (cases msg) 
        fix p' bool
        assume MsgIn :"(msg = <p', inM bool>)"
        with noInSends MsgIn MsgNoIn MsgEnabled 
          show "states = (states cfg2),
          msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })
             msg  states = (states cfg3),
              msgs = (((msgs cfg3) -# <pJ, inM False>) 
              ∪# {# <pJ, inM True> })"  
          using steps.simps(1) Step(2) select_convs(2) select_convs(1) 
          by auto
      next
        fix bool   
        assume "(msg = <⊥, outM bool>)"
        thus "states = (states cfg2),
          msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })
             msg  states = (states cfg3),
              msgs = (((msgs cfg3) -# <pJ, inM False>) 
              ∪# {# <pJ, inM True> })" 
          using steps_def Step(2) by auto
      next
        fix p v
        assume "(msg = <p, v>)"
        with noInSends MsgNoIn MsgEnabled show "states = (states cfg2),
          msgs = (((msgs cfg2) -# <pJ, inM False>) ∪# {# <pJ, inM True> })
             msg  states = (states cfg3),
              msgs = (((msgs cfg3) -# <pJ, inM False>) 
              ∪# {# <pJ, inM True> })" 
        using steps.simps(1) Step(2) select_convs(2) select_convs(1) by auto
      qed            
      with Cfg2 Step(3) show "qReachable cJ1 (Proc - {pJ})
        states = (states cfg3),
          msgs = (((msgs cfg3) -# <pJ, inM False>) ∪# {# <pJ, inM True> })" 
        using
          qReachable.simps[of "cJ1" "(Proc - {pJ})" 
          "states = (states cfg3),
          msgs = (((msgs cfg3) -# <pJ, inM False>) 
          ∪# {# <pJ, inM True> })"] by auto
    qed
  with CCQ(1) CCQ(2) InitMsgs StatescJcJ1 have CC':
    "withoutQReachable cJ1 {pJ} states = (states cc), 
      msgs = (((msgs cc) -# (<pJ,inM False>)) 
      ∪# {# (<pJ, inM True>)}) " by auto
  with QReachImplReach CJ1InitR initReachable_def reachable.simps 
    ReachableTrans
    have "initReachable states = (states cc), 
      msgs = (((msgs cc) -# (<pJ,inM False>)) 
      ∪# {# (<pJ, inM True>)}) " by meson
  with CC' have "False  val[pJ, cJ1]"
    unfolding pSilDecVal_def
    using CJ1InitR CC(1) select_convs(2) by auto
  hence "¬(vUniform True (cJ1))"
    unfolding vUniform_def
    using CJ1InitR by blast
  hence "nonUniform cJ1"
    using J(3) CJ1InitR unfolding cJ1_def by auto
  thus ?thesis
    using CJ1Init by blast
qed

text‹
  Völzer's Lemma 2 proves that for every process $p$ in the consensus setting 
  \isb{nonUniform} configurations can reach a configuration where the silent
  decision values of $p$ are True and False. This is key to the construction of
  non-deciding executions.

  \voelzer{Lemma 2}
›
lemma NonUniformCanReachSilentBivalence:
fixes 
  p:: 'p and
  c:: "('p, 'v, 's) configuration"
assumes 
  NonUni: "nonUniform c" and
  PseudoTermination: "cc Q . terminationPseudo 1 cc Q" and
  Agree: " cfg . reachable c cfg  agreement cfg"
shows 
   " c' . reachable c c'  val[p,c'] = {True, False}"
proof(cases "val[p,c] = {True, False}")
  case True 
  have "reachable c c" using reachable.simps by metis
  thus ?thesis
    using True by blast
next
  case False
  hence notEq: "val[p,c]  {True, False}" by simp
  from NonUni PseudoTermination DecisionValuesExist 
  have notE: "q. val[q,c]  {}" by simp  
  hence notEP: "val[p,c]  {}" by blast
  have valType: "q. val[q,c]  {True, False}" using pSilDecVal_def 
    by (metis (full_types) insertCI subsetI)
  hence "val[p,c]  {True, False}" by blast
  with notEq notEP  have "b:: bool. val[p,c] = {b}" by blast
  then obtain b where B: "val[p,c] = {b}" by auto
  from NonUni vUniform_def have 
    NonUni: "(q. val[q,c]  {True})  (q. val[q,c]  {False})" by simp
  have Bool: "b = True  b = False" by simp
  with NonUni have "q. val[q,c]  {b}" by blast
  then obtain q where Q: "val[q,c]  {b}" by auto
  from notE valType 
  have "val[q,c] = {True}  val[q,c] = {False}  val[q,c] = {True, False}" 
    by auto
  with Bool Q have "val[q,c] = {¬b}  val[q,c] = {b, ¬b}" by blast
  hence "(¬b)  val[q,c]" by blast
  with pSilDecVal_def 
  have " c'::('p, 'v, 's) configuration . (withoutQReachable c {q} c') 
    vDecided (¬b) c'" by simp
  then obtain c' where C': "withoutQReachable c {q} c'" "vDecided (¬b) c'" 
    by auto
  hence Reach: "reachable c c'" using QReachImplReach by simp
  have " cfg . reachable c' cfg  agreement cfg" 
  proof clarify
    fix cfg
    assume "reachable c' cfg"
    with Reach have "reachable c cfg" 
      using ReachableTrans[of c c'] by simp
    with Agree show "agreement cfg" by simp
  qed      
  with PseudoTermination C'(2) DecidedImpliesUniform have "vUniform (¬b) c'" 
    by simp
  hence notB: "val[p,c'] = {¬b}" using vUniform_def by simp
  with Reach B show " cfg. reachable c cfg  val[p,cfg] = {True, False}" 
  proof(induct rule: reachable.induct, simp)
    fix cfg1 cfg2 cfg3 msg
    assume
      IV: "val[p,cfg1] = {b} 
        val[p,cfg2] = {¬ b} 
          cfg::('p, 'v, 's) configuration. reachable cfg1 cfg 
           val[p,cfg] = {True, False}" and
      Reach:  "reachable cfg1 cfg2" and
      Step: "cfg2  msg  cfg3" and
      ValCfg1: "val[p,cfg1] = {b}" and
      ValCfg3: "val[p,cfg3] = {¬ b}"
    from ValCfg1 have InitCfg1: "initReachable cfg1" 
      using pSilDecVal_def by auto
    from Reach InitCfg1 initReachable_def reachable.simps ReachableTrans
      have InitCfg2: "initReachable cfg2" by blast
    with PseudoTermination DecisionValuesExist 
    have notE: "q. val[q,cfg2]  {}" by simp
    have valType: "q. val[q,cfg2]  {True, False}" using pSilDecVal_def
      by (metis (full_types) insertCI subsetI)
    from notE valType 
      have "val[p,cfg2] = {True}  val[p,cfg2] = {False} 
         val[p,cfg2] = {True, False}" 
      by auto
    with Bool have Val: "val[p,cfg2] = {b}  val[p,cfg2] = {¬b} 
       val[p,cfg2] = {True, False}" 
      by blast
    show "cfg::('p, 'v, 's) configuration. reachable cfg1 cfg 
       val[p,cfg] = {True, False}" 
    proof(cases "val[p,cfg2] = {b}")
      case True
      hence B: "val[p,cfg2] = {b}" by simp
      from Step have RecOrOut: "q. isReceiverOf q msg" by(cases msg, auto)
      then obtain q where Rec: "isReceiverOf q msg" by auto
      with B Step InitCfg2 SilentDecisionValueNotInverting 
      have "val[p,cfg3]  {¬b}" by simp
      with ValCfg3 have "False" by simp
      thus "cfg::('p, 'v, 's) configuration. reachable cfg1 cfg  
        val[p,cfg] = {True, False}" by simp
    next 
      case False
      with Val have Val: "val[p,cfg2] = {¬b}  val[p,cfg2] = {True, False}" 
        by simp
      show "cfg::('p, 'v, 's) configuration. reachable cfg1 cfg  
            val[p,cfg] = {True, False}" 
      proof(cases "val[p,cfg2] = {¬b}")
        case True
        hence "val[p,cfg2] = {¬b}" by simp
        with ValCfg1 IV show 
          "cfg::('p, 'v, 's) configuration. 
          reachable cfg1 cfg  val[p,cfg] = {True, False}" 
          by simp
      next
        case False
        with Val have "val[p,cfg2] = {True, False}" by simp
        with Reach have "reachable cfg1 cfg2  val[p,cfg2] = {True, False}" 
          by blast
        from this show "cfg::('p, 'v, 's) configuration. 
          reachable cfg1 cfg  val[p,cfg] = {True, False}" by blast
      qed
    qed
  qed
qed

end
end