Quelle  FLPSystem.thy

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