Theory AteProof

theory AteProof
imports AteDefs "../Reduction"
begin

context ate_parameters
begin

subsection ‹Preliminary Lemmas›

text ‹
  If a process newly decides value ‹v› at some round,
  then it received more than ‹E - α› messages holding ‹v›
  at this round.
›

lemma decide_sent_msgs_threshold:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nvp: "decide (rho r p) ≠ Some v"
  and vp: "decide (rho (Suc r) p) = Some v"
  shows "card {qq. sendMsg Ate_M r qq p (rho r qq) = v} > E - α"
proof -
  from run obtain μp
    where mu: "μp ∈ SHOmsgVectors Ate_M r p (rho r) (HOs r p) (SHOs r p)"
      and nxt: "nextState Ate_M r p (rho r p) μp (rho (Suc r) p)"
    by (auto simp: SHORun_eq SHOnextConfig_eq)
  from mu
  have "{qq. μp qq = Some v} - (HOs r p - SHOs r p)
          ⊆ {qq. sendMsg Ate_M r qq p (rho r qq) = v}"
       (is "?vrcvdp - ?ahop ⊆ ?vsentp") 
    by (auto simp: SHOmsgVectors_def)
  hence "card (?vrcvdp - ?ahop) ≤ card ?vsentp"
    and "card (?vrcvdp - ?ahop) ≥ card ?vrcvdp - card ?ahop"
    by (auto simp: card_mono diff_card_le_card_Diff)
  hence "card ?vsentp ≥ card ?vrcvdp - card ?ahop" by auto
  moreover
  from nxt nvp vp have "card ?vrcvdp > E"
    by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
  moreover
  from comm have "card (HOs r p - SHOs r p) ≤ α"
    by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
  ultimately
  show ?thesis using Egta by auto
qed

text ‹
  If more than ‹E - α› processes send a value ‹v› to some
  process ‹q› at some round, then ‹q› will receive at least
  ‹N + 2*α - E› messages holding ‹v› at this round. 
›

lemma other_values_received:
  assumes comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nxt: "nextState Ate_M r q (rho r q) μq ((rho (Suc r)) q)"
  and muq: "μq ∈ SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)"
  and vsent: "card {qq. sendMsg Ate_M r qq q (rho r qq) = v} > E - α"
             (is "card ?vsent > _")
  shows "card ({qq. μq qq ≠ Some v} ∩ HOs r q) ≤ N + 2*α - E"
proof -
  from nxt muq
  have "({qq. μq qq ≠ Some v} ∩ HOs r q) - (HOs r q - SHOs r q)
        ⊆  {qq. sendMsg Ate_M r qq q (rho r qq) ≠ v}"
    (is "?notvrcvd - ?aho ⊆ ?notvsent") 
    unfolding SHOmsgVectors_def by auto
  hence "card ?notvsent ≥ card (?notvrcvd - ?aho)"
    and "card (?notvrcvd - ?aho) ≥ card ?notvrcvd - card ?aho"
    by (auto simp: card_mono diff_card_le_card_Diff)
  moreover
  from comm have "card ?aho ≤ α"
    by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
  moreover
  have 1: "card ?notvsent + card ?vsent = card (?notvsent ∪ ?vsent)"
    by (subst card_Un_Int) auto
  have "?notvsent ∪ ?vsent = (UNIV::Proc set)" by auto
  hence "card (?notvsent ∪ ?vsent) = N" by simp
  with 1 vsent have "card ?notvsent ≤  N - (E + 1 - α)" by auto
  ultimately
  show ?thesis using EltN Egta by auto
qed

text ‹
  If more than ‹E - α› processes send a value ‹v› to some
  process ‹q› at some round ‹r›, and if ‹q› receives more than
  ‹T› messages in ‹r›, then ‹v› is the most frequently
  received value by ‹q› in ‹r›.
›

lemma mostOftenRcvd_v:
  assumes comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nxt: "nextState Ate_M r q (rho r q) μq ((rho (Suc r)) q)"
  and muq: "μq ∈ SHOmsgVectors Ate_M r q (rho r) (HOs r q) (SHOs r q)"
  and threshold_T: "card {qq. μq qq ≠ None} > T"
  and threshold_E: "card {qq. sendMsg Ate_M r qq q (rho r qq) = v} > E - α"
  shows "mostOftenRcvd μq = {v}"
proof -
  from muq have hodef:"HOs r q = {qq. μq qq ≠ None}"
    unfolding SHOmsgVectors_def by auto

  from comm nxt muq threshold_E
  have "card ({qq. μq qq ≠ Some v} ∩ HOs r q) ≤ N + 2*α - E"
    (is "card ?heardnotv ≤ _")
    by (rule other_values_received)
  moreover
  have "card ?heardnotv ≥ T + 1 - card {qq. μq qq = Some v}"
  proof -
    from muq
    have "?heardnotv = (HOs r q) - {qq. μq qq = Some v}"
      and "{qq. μq qq = Some v} ⊆ HOs r q"
      unfolding SHOmsgVectors_def by auto
    hence "card ?heardnotv = card (HOs r q) - card {qq. μq qq = Some v}"
      by (auto simp: card_Diff_subset)
    with hodef threshold_T show ?thesis by auto
  qed
  ultimately
  have "card {qq. μq qq = Some v} > card ?heardnotv"
    using TNaE by auto
  moreover
  {
    fix w
    assume w: "w ≠ v"
    with hodef have "{qq. μq qq = Some w} ⊆ ?heardnotv" by auto
    hence "card {qq. μq qq = Some w} ≤ card ?heardnotv" by (auto simp: card_mono)
  }
  ultimately
  have "{w. card {qq. μq qq = Some w} ≥ card {qq. μq qq = Some v}} = {v}"
    by force
  thus ?thesis unfolding mostOftenRcvd_def by auto
qed

text ‹
  If at some round more than ‹E - α› processes have their ‹x›
  variable set to ‹v›, then this is also true at next round.
›

lemma common_x_induct:
  assumes run: "SHORun Ate_M rho HOs SHOs" 
  and comm: "SHOcommPerRd Ate_M (HOs (r+k)) (SHOs (r+k))"
  and ih: "card {qq. x (rho (r + k) qq) = v} > E - α"
  shows "card {qq. x (rho (r + Suc k) qq) = v} > E - α"
proof -
  from ih 
  have thrE:"∀pp. card {qq. sendMsg Ate_M (r + k) qq pp (rho (r + k) qq) = v}
                      > E - α"
    by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)

  {
    fix qq
    assume kv:"x (rho (r + k) qq) = v"
    from run obtain μqq
      where nxt: "nextState Ate_M (r + k) qq (rho (r + k) qq) μqq ((rho (Suc (r + k))) qq)"
        and muq: "μqq ∈ SHOmsgVectors Ate_M (r + k) qq (rho (r + k)) 
                                         (HOs (r + k) qq) (SHOs (r + k) qq)"
      by (auto simp: SHORun_eq SHOnextConfig_eq)
        
    have "x (rho (r + Suc k) qq) = v"
    proof (cases "card {pp. μqq pp ≠ None} > T")
      case True
      with comm nxt muq thrE have "mostOftenRcvd μqq = {v}"
        by (auto dest: mostOftenRcvd_v)
      with nxt True show "x (rho (r + Suc k) qq) = v"
        by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
    next
      case False
      with nxt have "x (rho (r + Suc k) qq) = x (rho (r + k) qq)"
        by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
      with kv show "x (rho (r + Suc k) qq) = v" by simp
    qed
  }
  hence "{qq. x (rho (r + k) qq) = v} ⊆ {qq. x (rho (r + Suc k) qq) = v}"
    by auto
  hence "card {qq. x (rho (r + k) qq) = v} ≤ card {qq. x (rho (r + Suc k) qq) = v}"
    by (auto simp: card_mono)
  with ih show ?thesis by auto
qed

text ‹
  Whenever some process newly decides value ‹v›, then any
  process that updates its ‹x› variable will set it to ‹v›.
›
(* The proof mainly relies on lemmas @{text decide_sent_msgs_threshold},
   @{text mostOftenRcvd_v} and @{text common_x_induct}. *)

lemma common_x:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd (Ate_M::(Proc, 'val::linorder pstate, 'val) SHOMachine)
                              (HOs r) (SHOs r)"
  and d1: "decide (rho r p) ≠ Some v"
  and d2: "decide (rho (Suc r) p) = Some v"
  and qupdatex: "x (rho (r + Suc k) q) ≠ x (rho (r + k) q)"
  shows "x (rho (r + Suc k) q) = v"
proof -
  from comm 
  have "SHOcommPerRd (Ate_M::(Proc, 'val::linorder pstate, 'val) SHOMachine) 
                     (HOs (r+k)) (SHOs (r+k))" ..
  moreover
  from run obtain μq
    where nxt: "nextState Ate_M (r+k) q (rho (r+k) q) μq (rho (r + Suc k) q)"
      and muq: "μq ∈ SHOmsgVectors Ate_M (r+k) q (rho (r+k))
                                   (HOs (r+k) q) (SHOs (r+k) q)"
    by (auto simp: SHORun_eq SHOnextConfig_eq)
  moreover
  from nxt qupdatex 
  have threshold_T: "card {qq. μq qq ≠ None} > T"
    and xsmall: "x (rho (r + Suc k) q) = Min (mostOftenRcvd μq)"
    by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
  moreover
  have "E - α < card {qq. x (rho (r + k) qq) = v}"
  proof (induct k)
    from run comm d1 d2
    have "E - α < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}"
      by (auto dest: decide_sent_msgs_threshold)
    thus "E - α < card {qq. x (rho (r + 0) qq) = v}"
      by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
  next
    fix k
    assume "E - α < card {qq. x (rho (r + k) qq) = v}"
    with run comm show "E - α < card {qq. x (rho (r + Suc k) qq) = v}"
      by (auto dest: common_x_induct)
  qed
  with run
  have "E - α < card {qq. sendMsg Ate_M (r+k) qq q (rho (r+k) qq) = v}"
    by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def SHORun_eq SHOnextConfig_eq)
  ultimately
  have "mostOftenRcvd μq = {v}" by (auto dest:mostOftenRcvd_v)
  with xsmall show ?thesis by auto
qed

text ‹
  A process that holds some decision ‹v› has decided ‹v›
  sometime in the past.
›
lemma decisionNonNullThenDecided:
  assumes run: "SHORun Ate_M rho HOs SHOs"
      and dec: "decide (rho n p) = Some v"
  obtains m where "m < n"
              and "decide (rho m p) ≠ Some v"
              and "decide (rho (Suc m) p) = Some v"
proof -
  let "?dec k" = "decide (rho k p)"
  have "(∀m<n. ?dec (Suc m) ≠ ?dec m ⟶ ?dec (Suc m) ≠ Some v) ⟶ ?dec n ≠ Some v"
    (is "?P n" is "?A n ⟶ _")
  proof (induct n)
    from run show "?P 0"
      by (auto simp: Ate_SHOMachine_def SHORun_eq HOinitConfig_eq
                     initState_def Ate_initState_def)
  next
    fix n
    assume ih: "?P n" thus "?P (Suc n)" by force
  qed
  with dec that show ?thesis by auto
qed


subsection ‹Proof of Validity›

text ‹
  Validity asserts that if all processes were initialized with the same value,
  then no other value may ever be decided.
›

theorem ate_validity:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and initv: "∀q. x (rho 0 q) = v"
  and dp: "decide (rho r p) = Some w"
  shows "w = v"
proof -
  {
    fix r
    have "∀qq. sendMsg Ate_M r qq p (rho r qq) = v"
    proof (induct r)
      from run initv show "∀qq. sendMsg Ate_M 0 qq p (rho 0 qq) = v"
        by (auto simp: SHORun_eq SHOnextConfig_eq Ate_SHOMachine_def Ate_sendMsg_def)
    next
      fix r
      assume ih:"∀qq. sendMsg Ate_M r qq p (rho r qq) = v"

      have "∀qq. x (rho (Suc r) qq) = v"
      proof
        fix qq
        from run obtain μqq
          where nxt: "nextState Ate_M r qq (rho r qq) μqq (rho (Suc r) qq)"
            and mu: "μqq ∈ SHOmsgVectors Ate_M r qq (rho r) (HOs r qq) (SHOs r qq)"
          by (auto simp: SHORun_eq SHOnextConfig_eq)
        from nxt
        have "(card {pp. μqq pp ≠ None} > T ∧ x (rho (Suc r) qq) = Min (mostOftenRcvd μqq))
            ∨ (card {pp. μqq pp ≠ None} ≤ T ∧ x (rho (Suc r) qq) = x (rho r qq))"
          by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
        thus "x (rho (Suc r) qq) = v"
        proof safe
          assume "x (rho (Suc r) qq) = x (rho r qq)"
          with ih show "?thesis"
            by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
        next
          assume threshold_T:"T < card {pp. μqq pp ≠ None}"
             and xsmall:"x (rho (Suc r) qq) = Min (mostOftenRcvd μqq)"
                   
          have "card {pp. ∃w. w ≠ v ∧ μqq pp = Some w} ≤ T div 2"
          proof -
            from comm have 1:"card (HOs r qq - SHOs r qq) ≤ α"
              by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
            moreover
            from mu ih
            have "SHOs r qq ∩ HOs r qq ⊆ {pp. μqq pp = Some v}"
              and "HOs r qq = {pp. μqq pp ≠ None}"
              by (auto simp: SHOmsgVectors_def Ate_SHOMachine_def Ate_sendMsg_def)
            hence "{pp. μqq pp ≠ None} - {pp. μqq pp = Some v} 
                   ⊆ HOs r qq - SHOs r qq"
              by auto
            hence "card ({pp. μqq pp ≠ None} - {pp. μqq pp = Some v})
                      ≤ card (HOs r qq - SHOs r qq)"
              by (auto simp:card_mono)
            ultimately
            have "card ({pp. μqq pp ≠ None} - {pp. μqq pp = Some v}) ≤ T div 2"
              using Tge2a by auto
            moreover
            have "{pp. μqq pp ≠ None} - {pp. μqq pp = Some v}
                  = {pp. ∃w. w ≠ v ∧ μqq pp = Some w}" by auto
            ultimately
            show ?thesis by simp
          qed
          moreover
          have "{pp. μqq pp ≠ None}
                = {pp. μqq pp = Some v} ∪ {pp. ∃w. w ≠ v ∧ μqq pp = Some w}"
            and "{pp. μqq pp = Some v} ∩ {pp. ∃w. w ≠ v ∧ μqq pp = Some w} = {}" 
            by auto
          hence "card {pp. μqq pp ≠ None}
                 = card {pp. μqq pp = Some v} + card {pp. ∃w. w ≠ v ∧ μqq pp = Some w}"
            by (auto simp: card_Un_Int)
          moreover
          note threshold_T
          ultimately
          have "card {pp. μqq pp = Some v} > card {pp. ∃w. w ≠ v ∧ μqq pp = Some w}"
            by auto
          moreover
          {
            fix w
            assume "w ≠ v"
            hence "{pp. μqq pp = Some w} ⊆ {pp. ∃w. w ≠ v ∧ μqq pp = Some w}" 
              by auto
            hence "card {pp. μqq pp = Some w} ≤ card {pp. ∃w. w ≠ v ∧ μqq pp = Some w}"
              by (auto simp: card_mono)
          }
          ultimately
          have zz:"⋀w. w ≠ v ⟹ 
                       card {pp. μqq pp = Some w} < card {pp. μqq pp = Some v}"
            by force
          hence "⋀w. card {pp. μqq pp = Some v} ≤ card {pp. μqq pp = Some w}
                      ⟹ w = v" 
            by force
          with zz have "mostOftenRcvd μqq = {v}"
            by (force simp: mostOftenRcvd_def)
          with xsmall show "x (rho (Suc r) qq) = v" by auto
        qed
      qed
      thus "∀qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v"
        by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
    qed
  }
  note P = this

  from run dp obtain rp
    where rp: "rp < r" "decide (rho rp p) ≠ Some w" 
              "decide (rho (Suc rp) p) = Some w"
    by (rule decisionNonNullThenDecided)

  from run obtain μp
    where nxt: "nextState Ate_M rp p (rho rp p) μp (rho (Suc rp) p)"
      and mu: "μp ∈ SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)"
    by (auto simp: SHORun_eq SHOnextConfig_eq)

  {
    fix w
    assume w: "w ≠ v"
    from comm have "card (HOs rp p - SHOs rp p) ≤ α"
      by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
    moreover
    from mu P
    have "SHOs rp p ∩ HOs rp p ⊆ {pp. μp pp = Some v}"
      and "HOs rp p = {pp. μp pp ≠ None}"
      by (auto simp: SHOmsgVectors_def)
    hence "{pp. μp pp ≠ None} - {pp. μp pp = Some v}
           ⊆ HOs rp p - SHOs rp p"
      by auto
    hence "card ({pp. μp pp ≠ None} - {pp. μp pp = Some v})
            ≤ card (HOs rp p - SHOs rp p)"
      by (auto simp: card_mono)
    ultimately
    have "card ({pp. μp pp ≠ None} - {pp. μp pp = Some v}) < E"
      using Egta by auto
    moreover
    from w have "{pp. μp pp = Some w} 
                 ⊆ {pp. μp pp ≠ None} - {pp. μp pp = Some v}"
      by auto
    hence "card {pp. μp pp = Some w} 
             ≤ card ({pp. μp pp ≠ None} - {pp. μp pp = Some v})"
      by (auto simp: card_mono)
    ultimately
    have "card {pp. μp pp = Some w} < E" by simp
  }
  hence PP: "⋀w. card {pp. μp pp = Some w} ≥ E ⟹ w = v" by force

  from rp nxt mu have "card {q. μp q = Some w} > E"
    by (auto simp: SHOmsgVectors_def Ate_SHOMachine_def 
                   nextState_def Ate_nextState_def)
  with PP show ?thesis by auto
qed


subsection ‹Proof of Agreement›

text ‹
  If two processes decide at the some round, they decide the same value.
›
(* The proof mainly relies on lemma @{text decide_sent_msgs_threshold}. *)

lemma common_decision:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nvp: "decide (rho r p) ≠ Some v"
  and vp: "decide (rho (Suc r) p) = Some v"
  and nwq: "decide (rho r q) ≠ Some w"
  and wq: "decide (rho (Suc r) q) = Some w"
  shows "w = v"
proof -
  have gtn: "card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
             + card {qq. sendMsg Ate_M r qq q (rho r qq) = w} > N"
  proof -
    from run comm nvp vp
    have "card {qq. sendMsg Ate_M r qq p (rho r qq) = v} > E - α"
      by (rule decide_sent_msgs_threshold)
    moreover
    from run comm nwq wq
    have "card {qq. sendMsg Ate_M r qq q (rho r qq) = w} > E - α"
      by (rule decide_sent_msgs_threshold)
    ultimately
    show ?thesis using majE by auto
  qed

  show ?thesis
  proof (rule ccontr)
    assume vw:"w ≠ v"
    have "∀qq. sendMsg Ate_M r qq p (rho r qq) = sendMsg Ate_M r qq q (rho r qq)"
      by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
    with vw
    have "{qq. sendMsg Ate_M r qq p (rho r qq) = v}
          ∩ {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}"
      by auto
    with gtn
    have "card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} 
                 ∪ {qq. sendMsg Ate_M r qq q (rho r qq) = w}) > N"
      by (auto simp: card_Un_Int)
    moreover
    have "card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} 
                 ∪ {qq. sendMsg Ate_M r qq q (rho r qq) = w}) ≤ N"
      by (auto simp: card_mono)
    ultimately
    show "False" by auto
  qed
qed

text ‹
  If process ‹p› decides at step ‹r› and process ‹q› decides
  at some later step ‹r+k› then ‹p› and ‹q› decide the
  same value.
›
(*
  The proof mainly relies on lemmas @{text common_decision}, @{text common_x},
  @{text decide_with_threshold_E}, @{text unique_majority_E_α} 
  and @{text  decide_sent_msgs_threshold}.
*)

lemma laterProcessDecidesSameValue :
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nd1: "decide (rho r p) ≠ Some v"
  and d1: "decide (rho (Suc r) p) = Some v"
  and nd2: "decide (rho (r+k) q) ≠ Some w"
  and d2: "decide (rho (Suc (r+k)) q) = Some w"
  shows "w = v"
proof (rule ccontr)
  assume vdifw:"w ≠ v"
  have kgt0: "k > 0"
  proof (rule ccontr)
    assume "¬ k > 0"
    hence "k = 0" by auto
    with run comm nd1 d1 nd2 d2 have "w = v"
      by (auto dest: common_decision)
    with vdifw show False ..
  qed

  have 1: "{qq. sendMsg Ate_M r qq p (rho r qq) = v}
           ∩ {qq. sendMsg Ate_M (r+k) qq q (rho (r+k) qq) = w} = {}"
    (is "?sentv ∩ ?sentw = {}")
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain qq
      where xrv: "x (rho r qq) = v" and rkw: "x (rho (r+k) qq) = w"
      by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
    have "∃k' < k. x (rho (r + k') qq) ≠ w ∧ x (rho (r + Suc k') qq) = w"
    proof (rule ccontr)
      assume f: "¬ ?thesis"
      {
        fix k'
        assume kk':"k' < k" hence "x (rho (r + k') qq) ≠ w"
        proof (induct k')
          from xrv vdifw
          show "x (rho (r + 0) qq) ≠ w" by simp
        next
          fix k'
          assume ih:"k' < k ⟹ x (rho (r + k') qq) ≠ w"
             and ksk':"Suc k' < k"
          from ksk' have "k' < k" by simp
          with ih f  show "x (rho (r + Suc k') qq) ≠ w" by auto
        qed
      }
      with f have "∀k' < k. x (rho (r + Suc k') qq) ≠ w" by auto
      moreover
      from kgt0 have "k - 1 < k" and kk:"Suc (k - 1) = k" by auto
      ultimately
      have "x (rho (r + Suc (k - 1)) qq) ≠ w" by blast
      with rkw kk show "False" by simp
    qed
    then obtain k'
      where "k' < k" 
        and w: "x (rho (r + Suc k') qq) = w"
        and qqupdatex: "x (rho (r + Suc k') qq) ≠ x (rho (r + k') qq)" 
      by auto
    from run comm nd1 d1 qqupdatex
    have "x (rho (r + Suc k') qq) = v" by (rule common_x)
    with w vdifw show False by simp
  qed
  from run comm nd1 d1 have sentv: "card ?sentv > E - α"
    by (auto dest: decide_sent_msgs_threshold)
  from run comm nd2 d2 have "card ?sentw > E - α"
    by (auto dest: decide_sent_msgs_threshold)
  with sentv majE have "(card ?sentv) + (card ?sentw) > N"
    by simp
  with 1 vdifw  have 2: "card (?sentv ∪ ?sentw) > N"
    by (auto simp: card_Un_Int)
  have "card (?sentv ∪ ?sentw) ≤ N"
    by (auto simp: card_mono)
  with 2 show "False" by simp
qed

text ‹
  The Agreement property is now an immediate consequence.
›
(*
  The proof mainly relies on lemmas @{text decisionNonNullThenDecided}
  and @{text laterProcessDecidesSameValue}.
*)

theorem ate_agreement:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and p: "decide (rho m p) = Some v"
  and q: "decide (rho n q) = Some w"
  shows "w = v"
proof -
  from run p obtain k where
    k: "k < m" "decide (rho k p) ≠ Some v" "decide (rho (Suc k) p) = Some v"
    by (rule decisionNonNullThenDecided)
  from run q obtain l where
    l: "l < n" "decide (rho l q) ≠ Some w" "decide (rho (Suc l) q) = Some w"
    by (rule decisionNonNullThenDecided)
  show ?thesis
  proof (cases "k ≤ l")
    case True
    then obtain i where "l = k+i" by (auto simp add: le_iff_add)
    with run comm k l show ?thesis
      by (auto dest: laterProcessDecidesSameValue)
  next
    case False
    hence "l ≤ k" by simp
    then obtain i where m: "k = l+i" by (auto simp add: le_iff_add)
    with run comm k l show ?thesis
      by (auto dest: laterProcessDecidesSameValue)
  qed
qed


subsection ‹Proof of Termination›

text ‹
  We now prove that every process must eventually decide, given the
  global and round-by-round communication predicates.
›
(* The proof relies on previous lemmas @{text common_x_induct} and @{text mostOftenRcvd_v}. *)

theorem ate_termination:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and commR: "∀r. (SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine)
                                     ⇒ (Proc HO) ⇒ (Proc HO) ⇒ bool) 
                  Ate_M (HOs r) (SHOs r)"
  and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "∃r v. decide (rho r p) = Some v"
proof -
  from commG obtain r' π1 π2
    where πea: "card π1 > E - α"
      and πt: "card π2 > T"
      and  hosho: "∀p ∈ π1. (HOs r' p = π2 ∧ SHOs r' p ∩ HOs r' p = π2)"
    by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)

  obtain v where
    P1: "∀pp. card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} > E - α"
  proof -
    have "∀p ∈ π1. ∀q ∈ π1. x (rho (Suc r') p) = x (rho (Suc r') q)"
    proof (clarify)
      fix p q
      assume p: "p ∈ π1" and q: "q ∈ π1"

      from run obtain μp
        where nxtp: "nextState Ate_M r' p (rho r' p) μp (rho (Suc r') p)"
          and mup: "μp ∈ SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)"
        by (auto simp: SHORun_eq SHOnextConfig_eq)

      from run obtain μq
        where nxtq: "nextState Ate_M r' q (rho r' q) μq (rho (Suc r') q)"
          and muq: "μq ∈ SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)"
        by (auto simp: SHORun_eq SHOnextConfig_eq)

      from mup muq p q
      have "{qq. μq qq ≠ None}  = HOs r' q"
        and 2:"{qq. μq qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
               ⊇ SHOs r' q ∩ HOs r' q"
        and "{qq. μp qq ≠ None}  = HOs r' p"
        and 4:"{qq. μp qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
               ⊇ SHOs r' p ∩ HOs r' p"
        by (auto simp: SHOmsgVectors_def)
      with p q hosho 
      have aa:"π2 = {qq. μq qq ≠ None}"
        and cc:"π2 = {qq. μp qq ≠ None}" by auto
      from p q hosho 2
      have bb:"{qq. μq qq = Some (sendMsg Ate_M r' qq q (rho r' qq))} ⊇ π2"
        by auto
      from p q hosho 4
      have dd:"{qq. μp qq = Some (sendMsg Ate_M r' qq p (rho r' qq))} ⊇ π2" 
        by auto
      have "Min (mostOftenRcvd μp) = Min (mostOftenRcvd μq)"
      proof -
        have "∀qq. sendMsg Ate_M r' qq p (rho r' qq)
                   = sendMsg Ate_M r' qq q (rho r' qq)"
          by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
        with aa bb cc dd have "∀qq. μp qq ≠ None ⟶ μp qq = μq qq"
          by force
        moreover
        from aa bb cc dd
        have "{qq. μp qq ≠ None} = {qq. μq qq ≠ None}" by auto
        hence "∀qq. μp qq = None ⟷ μq qq = None" by blast
        hence "∀qq. μp qq = None ⟶ μp qq = μq qq" by auto
        ultimately
        have "∀qq. μp qq = μq qq" by blast
        thus ?thesis by (auto simp: mostOftenRcvd_def)
      qed
      with πt aa nxtq πt cc nxtp
      show "x (rho (Suc r') p) = x (rho (Suc r') q)"
        by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
    qed
    then obtain v where Pv:"∀p ∈ π1. x (rho (Suc r') p) = v" by blast
    {
      fix pp
      from Pv have "∀p ∈ π1. sendMsg Ate_M (Suc r') p pp (rho (Suc r') p) = v"
        by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
      hence "card π1 ≤ card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}"
        by (auto intro: card_mono)
      with πea
      have "E - α < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}"
        by simp
    }
    with that show ?thesis by blast
  qed

  {
    fix k pp
    have "E - α < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}"
      (is "?P k")
    proof (induct k)
      from P1 show "?P 0" by simp
    next
      fix k
      assume ih: "?P k"
      from commR
      have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine) 
                               ⇒ (Proc HO) ⇒ (Proc HO) ⇒ bool) 
                Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))" ..
      moreover
      from ih have "E - α < card {qq. x (rho (Suc r' + k) qq) = v}"
        by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
      ultimately
      have "E - α < card {qq. x (rho (Suc r' + Suc k) qq) = v}"
        by (rule common_x_induct[OF run])
      thus "?P (Suc k)"
        by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
    qed
  }
  note P2 = this

  {
    fix k pp
    assume ppupdatex: "x (rho (Suc r' + Suc k) pp) ≠ x (rho (Suc r' + k) pp)"

    from commR 
    have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine)
                            ⇒ (Proc HO) ⇒ (Proc HO) ⇒ bool)
              Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))" ..
    moreover
    from run obtain μpp
      where nxt:"nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) μpp 
                           (rho (Suc r' + Suc k) pp)"
        and mu: "μpp ∈ SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k))
                           (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)"
      by (auto simp: SHORun_eq SHOnextConfig_eq)
    moreover
    from nxt ppupdatex
    have threshold_T: "card {qq. μpp qq ≠ None} > T"
      and xsmall: "x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd μpp)"
      by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
    moreover
    from P2
    have "E - α < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}" .
    ultimately
    have "mostOftenRcvd μpp = {v}" by (auto dest!: mostOftenRcvd_v)
    with xsmall 
    have "x (rho (Suc r' + Suc k) pp) = v" by simp
  }
  note P3 = this

  have P4:"∀pp. ∃k. x (rho (Suc r' + Suc k) pp) = v"
  proof
    fix pp
    from commG have "∃r'' > r'. card (HOs r'' pp) > T"
      by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)
    then obtain k where "Suc r' + k > r'" and t:"card (HOs (Suc r' + k) pp) > T"
      by (auto dest: less_imp_Suc_add)
    moreover
    from run obtain μpp
      where nxt: "nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) μpp
                                  (rho (Suc r' + Suc k) pp)"
        and mu: "μpp ∈ SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k))
                                  (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)"
      by (auto simp: SHORun_eq SHOnextConfig_eq)
    moreover
    have "x (rho (Suc r' + Suc k) pp) = v"
    proof -
      from commR
      have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val::linorder) SHOMachine)
                                ⇒ (Proc HO) ⇒ (Proc HO) ⇒ bool) 
                Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))" ..
      moreover
      from mu have "HOs (Suc r' + k) pp = {q. μpp q ≠ None}"
        by (auto simp: SHOmsgVectors_def)
      with nxt t
      have threshold_T: "card {q. μpp q ≠ None} > T"
        and xsmall: "x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd μpp)"
        by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
      moreover
      from P2
      have "E - α < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}" .
      ultimately
      have "mostOftenRcvd μpp = {v}"  
        using nxt mu by (auto dest!: mostOftenRcvd_v)
      with xsmall show ?thesis by auto
    qed
    thus "∃k. x (rho (Suc r' + Suc k) pp) = v" ..
  qed

  have P5a: "∀pp. ∃rr. ∀k. x (rho (rr + k) pp) = v"
  proof
    fix pp
    from P4 obtain rk where
      xrrv: "x (rho (Suc r' + Suc rk) pp) = v" (is "x (rho ?rr pp) = v")
      by blast
    have "∀k. x (rho (?rr + k) pp) = v"
    proof
      fix k
      show "x (rho (?rr + k) pp) = v" 
      proof (induct k)
        from xrrv show "x (rho (?rr + 0) pp) = v" by simp
      next
        fix k
        assume ih: "x (rho (?rr + k) pp) = v"
        obtain k' where rrk: "Suc r' + k' = ?rr + k" by auto
        show "x (rho (?rr + Suc k) pp) = v"
        proof (rule ccontr)
          assume nv: "x (rho (?rr + Suc k) pp) ≠ v"
          with rrk ih
          have "x (rho (Suc r' + Suc k') pp) ≠ x (rho (Suc r' + k') pp)"
            by (simp add: ac_simps)
          hence "x (rho (Suc r' + Suc k') pp) = v" by (rule P3)
          with rrk nv show False by (simp add: ac_simps)
        qed
      qed
    qed
    thus "∃rr. ∀k. x (rho (rr + k) pp) = v" by blast
  qed

  from P5a have "∃F. ∀pp k. x (rho (F pp + k) pp) = v" by (rule choice)
  then obtain R::"(Proc ⇒ nat)"
    where imgR: "R ` (UNIV::Proc set) ≠ {}"
      and R: "∀pp k. x (rho (R pp + k) pp) = v" 
    by blast
  define rr where "rr = Max (R ` UNIV)"

  have P5: "∀r' > rr. ∀pp. x (rho r' pp) = v"
  proof (clarify)
    fix r' pp
    assume r': "r' > rr"
    hence "r' > R pp" by (auto simp: rr_def)
    then obtain i where "r' = R pp + i"
      by (auto dest: less_imp_Suc_add)
    with R show "x (rho r' pp) = v" by auto
  qed

  from commG have "∃r' > rr. card (SHOs r' p ∩ HOs r' p) > E"
    by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)
  with P5 obtain r'
    where "r' > rr"
      and "card (SHOs r' p ∩ HOs r' p) > E"
      and "∀pp. sendMsg Ate_M r' pp p (rho r' pp) = v"
    by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
  moreover
  from run obtain μp
    where nxt: "nextState Ate_M r' p (rho r' p) μp (rho (Suc r') p)"
      and mu: "μp ∈ SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)"
    by (auto simp: SHORun_eq SHOnextConfig_eq)
  from mu 
  have "card (SHOs r' p ∩ HOs r' p)
        ≤ card {q. μp q = Some (sendMsg Ate_M r' q p (rho r' q))}"
    by (auto simp: SHOmsgVectors_def intro: card_mono)
  ultimately
  have threshold_E: "card {q. μp q = Some v} > E" by auto
  with nxt show ?thesis
    by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
qed


subsection ‹\ate{} Solves Weak Consensus›

text ‹
  Summing up, all (coarse-grained) runs of \ate{} for
  HO and SHO collections that satisfy the communication predicate 
  satisfy the Weak Consensus property.
›

theorem ate_weak_consensus:
  assumes run: "SHORun Ate_M rho HOs SHOs"
      and commR: "∀r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "weak_consensus (x ∘ (rho 0)) decide rho"
  unfolding weak_consensus_def using assms
  by (auto elim: ate_validity ate_agreement ate_termination)

text ‹
  By the reduction theorem, the correctness of the algorithm carries over
  to the fine-grained model of runs.
›

theorem ate_weak_consensus_fg:
  assumes run: "fg_run Ate_M rho HOs SHOs (λr q. undefined)"
      and commR: "∀r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "weak_consensus (λp. x (state (rho 0) p)) decide (state ∘ rho)"
    (is "weak_consensus ?inits _ _")
proof (rule local_property_reduction[OF run weak_consensus_is_local])
  fix crun
  assume crun: "CSHORun Ate_M crun HOs SHOs (λr q. undefined)"
     and init: "crun 0 = state (rho 0)"
  from crun have "SHORun Ate_M crun HOs SHOs" by (unfold SHORun_def)
  from this commR commG 
  have "weak_consensus (x ∘ (crun 0)) decide crun"
    by (rule ate_weak_consensus)
  with init show "weak_consensus ?inits decide crun"
    by (simp add: o_def)
qed

end   ― ‹context @{text "ate_parameters"}›

end   (* theory AteProof *)