theory EWD840
  imports "HOL-TLA.TLA"
begin

section Utilities

text ‹A handful of general lemmas that were useful along the way.›

lemma temp_impI:
  assumes "sigma ⊨ P ⟹ sigma ⊨ Q"
  shows "sigma ⊨ P ⟶ Q"
  using assms by simp

lemma imp_leadsto_reflexive: "⊢ S ⟶ (F ↝ F)" using LatticeReflexivity [where F = F] by auto

lemma imp_leadsto_transitive:
  assumes "⊢ S ⟶ (F ↝ G)" "⊢ S ⟶ (G ↝ H)"
  shows "⊢ S ⟶ (F ↝ H)"
proof (intro tempI temp_impI)
  fix sigma
  assume S: "S sigma"
  with assms have 1: "sigma ⊨ (F ↝ G)" "sigma ⊨ (G ↝ H)"
    by (auto simp add: Valid_def)

  from 1 LatticeTransitivity [where F = F and G = G and H = H]
  show "sigma ⊨ F ↝ H"
    by (auto simp add: Valid_def)
qed

lemma imp_leadsto_diamond:
  assumes "⊢ S ⟶ (A ↝ (B ∨ C))"
  assumes "⊢ S ⟶ (B ↝ D)"
  assumes "⊢ S ⟶ (C ↝ D)"
  shows   "⊢ S ⟶ (A ↝ D)"
proof (intro tempI temp_impI)
  fix sigma
  assume S: "sigma ⊨ S"
  with assms have
    ABC: "sigma ⊨ A ↝ (B ∨ C)" and
    BD:  "sigma ⊨ B ↝ D" and
    CD:  "sigma ⊨ C ↝ D"
    by (auto simp add: Valid_def)
  with LatticeDiamond [where A = A and B = B and C = C and D = D]
  show "sigma ⊨ A ↝ D"
    by (auto simp add: Valid_def)
qed

lemma temp_conj_eq_imp:
  assumes "⊢ P ⟶ (Q = R)"
  shows "⊢ (P ∧ Q) = (P ∧ R)"
  using assms by (auto simp add: Valid_def)

text ‹The following lemma is particularly useful for a system that makes
some progress which either reaches the desired state directly or which leaves it in
a state that is definitely not the desired state but from which it can reach the desired state via
some further progress.›

lemma imp_leadsto_triangle_excl:
  assumes AB: "⊢ S ⟶ (A ↝ B)"
  assumes BC: "⊢ S ⟶ ((B ∧ ¬C) ↝ C)"
  shows "⊢ S ⟶ (A ↝ C)"
proof -
  have "⊢ ((B ∧ ¬C) ∨ (B ∧ C)) = B" by auto
  from inteq_reflection [OF this] AB have ABCBC: "⊢ S ⟶ (A ↝ ((B ∧ ¬C) ∨ (B ∧ C)))" by simp

  show ?thesis
  proof (intro imp_leadsto_diamond [OF ABCBC] BC)
    from ImplLeadsto_simple [where F = "LIFT (B ∧ C)"]
    show "⊢ S ⟶ (B ∧ C ↝ C)"
      by (auto simp add: Valid_def)
  qed
qed

text ‹An action that updates a single value of a function.›

definition updatedFun :: "('a ⇒ 'b) stfun ⇒ 'a ⇒ 'b trfun ⇒ action" where
  "updatedFun f x v ≡ ACT (∀n. id<f$,#n> = (if #n = #x then v else id<$f,#n>))"

section Nodes

text ‹There is a fixed, finite, set of nodes, which are numbered. Introduce a distinct type
for node identifiers, and an ordering relation, and an induction principle.›

axiomatization NodeCount :: nat where NodeCount_positive: "NodeCount > 0"

typedef Node = "{0..<NodeCount}" using NodeCount_positive by auto

definition FirstNode    :: Node where "FirstNode == Abs_Node 0"
definition LastNode     :: Node where "LastNode  == Abs_Node (NodeCount-1)"
definition PreviousNode :: "Node ⇒ Node" where "PreviousNode == λn. Abs_Node (Rep_Node n - 1)"

instantiation Node :: linorder
begin
definition less_eq_Node :: "Node ⇒ Node ⇒ bool" where "n ≤ m ≡ Rep_Node n ≤ Rep_Node m"
definition less_Node    :: "Node ⇒ Node ⇒ bool" where "n < m ≡ Rep_Node n < Rep_Node m"

instance proof
  show "⋀(x::Node) y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)" using less_Node_def less_eq_Node_def by force
  show "⋀(x::Node). x ≤ x" using less_eq_Node_def by force
  show "⋀(x::Node) y z. x ≤ y ⟹ y ≤ z ⟹ x ≤ z" using less_eq_Node_def by force
  show "⋀(x::Node) y. x ≤ y ∨ y ≤ x" using less_eq_Node_def by force
  show "⋀(x::Node) y. x ≤ y ⟹ y ≤ x ⟹ x = y" using less_Node_def less_eq_Node_def
    by (simp add: Rep_Node_inject)
qed
end

lemma PreviousNode_fixed_point:
  assumes "n = PreviousNode n"
  shows "n = FirstNode"
  using assms
  unfolding PreviousNode_def FirstNode_def
  by (metis Abs_Node_inject One_nat_def Rep_Node Rep_Node_inverse atLeastLessThan_iff cancel_comm_monoid_add_class.diff_cancel diff_Suc_less diff_le_self le_less_trans le_neq_implies_less not_le)

lemma Node_gt_PreviousNode:
  assumes "n ≠ FirstNode"
  shows "m > (PreviousNode n) = (m > n ∨ m = n)"
  using assms unfolding PreviousNode_def less_Node_def FirstNode_def
  by (smt Abs_Node_inverse Rep_Node Rep_Node_inject atLeastLessThan_iff diff_Suc_1 diff_is_0_eq' diff_le_self le_add_diff_inverse less_Suc_eq_le not_le_imp_less not_less_iff_gr_or_eq)

lemma Node_gt_ne: "(m::Node) > n ⟹ m ≠ n" unfolding less_Node_def by blast

lemma Node_gt_LastNode [simp]: "n > LastNode = False"
  unfolding LastNode_def less_Node_def
  using Abs_Node_inverse NodeCount_positive Rep_Node not_less_eq by auto

lemma Node_induct [case_names FirstNode PreviousNode]:
  assumes FirstNode: "P FirstNode"
  assumes PreviousNode: "⋀n. n ≠ FirstNode ⟹ P (PreviousNode n) ⟹ P n"
  shows "P n"
proof -
  define n_num where "n_num == Rep_Node n"
  have n_eq: "n = Abs_Node n_num"
    by (simp add: Rep_Node_inverse n_num_def)

  have "n_num < NodeCount" using Rep_Node n_num_def by auto
  thus ?thesis
    unfolding n_eq
  proof (induct n_num)
    case 0 with FirstNode show ?case by (simp add: FirstNode_def)
  next
    case (Suc n_num)
    hence hyp: "P (Abs_Node n_num)" by auto

    show ?case
    proof (rule PreviousNode)
      show "Abs_Node (Suc n_num) ≠ FirstNode" unfolding FirstNode_def
        by (simp add: Abs_Node_inject NodeCount_positive Suc.prems)
      from hyp Suc.prems show " P (PreviousNode (Abs_Node (Suc n_num)))"
        unfolding PreviousNode_def by (simp add: Abs_Node_inverse)
    qed
  qed
qed

datatype TerminationState = MaybeTerminated | NotTerminated

axiomatization
  isNodeActive  :: "(Node ⇒ bool) stfun" and
  nodeState     :: "(Node ⇒ TerminationState) stfun" and
  tokenPosition :: "Node stfun" and
  tokenState    :: "TerminationState stfun"
  where
  ewd_basevars: "basevars (isNodeActive, nodeState, tokenPosition, tokenState)"

definition StartState :: stpred where
  "StartState == PRED tokenPosition = #FirstNode ∧ tokenState = #NotTerminated"

definition InitiateProbe :: action where
  "InitiateProbe == ACT
    (($tokenPosition = #FirstNode)
    ∧ ($tokenState = #NotTerminated ∨ id<$nodeState,#FirstNode> = #NotTerminated)
    ∧ tokenPosition$ = #LastNode
    ∧ tokenState$ = #MaybeTerminated
    ∧ (unchanged isNodeActive)
    ∧ (updatedFun nodeState FirstNode (const MaybeTerminated)))"

definition PassToken :: "Node ⇒ action" where
  "PassToken i == ACT
    (($tokenPosition = #i)
    ∧ ($tokenPosition ≠ #FirstNode)
    ∧ (¬ id<$isNodeActive,#i> ∨ id<$nodeState,#i> = #NotTerminated ∨ $tokenState = #NotTerminated)
    ∧ (tokenPosition$ = PreviousNode<$tokenPosition>)
    ∧ (tokenState$ = (if id<$nodeState,#i> = #NotTerminated then #NotTerminated else $tokenState))
    ∧ (unchanged isNodeActive)
    ∧ (updatedFun nodeState i (const MaybeTerminated)))"

definition SendMsg :: "Node ⇒ action" where
  "SendMsg i == ACT
    id<$isNodeActive,#i>
    ∧ (∃ j. #j ≠ #i ∧ (updatedFun isNodeActive j (const True))
                     ∧ (updatedFun nodeState i (ACT if #i < #j then #NotTerminated else id<$nodeState,#i>)))
    ∧ unchanged (tokenPosition, tokenState)"

definition Deactivate :: "Node ⇒ action" where
  "Deactivate i == ACT
    id<$isNodeActive,#i>
    ∧ (updatedFun isNodeActive i (const False))
    ∧ unchanged (tokenPosition, tokenState, nodeState)"

definition Controlled :: action where
  "Controlled ≡ ACT (InitiateProbe ∨ (∃ n. PassToken n))"

definition Environment :: action where
  "Environment ≡ ACT (∃ n. SendMsg n ∨ Deactivate n)"

definition Next :: action where
  "Next ≡ ACT (Controlled ∨ Environment)"

definition Fairness :: temporal where
  "Fairness ≡ TEMP WF(Controlled)_(isNodeActive,nodeState,tokenPosition,tokenState)"

definition Spec :: temporal where
  "Spec ≡ TEMP (Init StartState ∧ □[Next]_(isNodeActive,nodeState,tokenPosition,tokenState) ∧ Fairness)"

definition TerminationDetected :: stpred where
  "TerminationDetected ≡ PRED
    (tokenPosition = #FirstNode
    ∧ tokenState = #MaybeTerminated
    ∧ id<nodeState,#FirstNode> = #MaybeTerminated
    ∧ ¬ id<isNodeActive,#FirstNode>)"

lemma angle_Controlled_lifted: "⊢ <Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState) = Controlled"
  unfolding angle_def Controlled_def InitiateProbe_def PassToken_def updatedFun_def
  using PreviousNode_fixed_point by auto

lemmas angle_Controlled = inteq_reflection [OF angle_Controlled_lifted]

lemma basevars_arbitrary:
  assumes "⋀u. ⟦ tokenPosition u = A; tokenState u = B; isNodeActive u = C; nodeState u = D ⟧ ⟹ P"
  shows P
  using assms ewd_basevars unfolding basevars_def surj_def apply auto by metis

lemma enabled_controlled_lifted:
  "⊢ Enabled Controlled
      = (tokenState = #NotTerminated ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ (tokenPosition ≠ #FirstNode ∧ ¬ id<isNodeActive, tokenPosition>))"
proof -
  have 1: "⊢ Enabled Controlled = (Enabled InitiateProbe ∨ Enabled (∃n. PassToken n))"
    unfolding Controlled_def
    using enabled_disj by simp

  have 2: "⊢ Enabled InitiateProbe = (tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated))"
  proof (intro intI)
    fix w
    show "w ⊨ Enabled InitiateProbe = (tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated))"
      apply (rule basevars_arbitrary [of LastNode MaybeTerminated "isNodeActive w" "λn. if n = FirstNode then MaybeTerminated else nodeState w n"])
      unfolding InitiateProbe_def enabled_def updatedFun_def
      by auto
  qed

  have 3: "⊢ Enabled (∃n. PassToken n) = ((tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))"
  proof (intro intI)
    fix w
    show "w ⊨ Enabled (∃n. PassToken n) = ((tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))"
      apply (rule basevars_arbitrary [of "PreviousNode (tokenPosition w)" "if nodeState w (tokenPosition w) = NotTerminated then NotTerminated else tokenState w" "isNodeActive w" "λn. if n = tokenPosition w then MaybeTerminated else nodeState w n"])
      unfolding PassToken_def enabled_def updatedFun_def
      by auto
  qed

  have 4:
    "⊢ Enabled Controlled = ((tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated))
          ∨ (tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))"
    unfolding inteq_reflection [OF 1]
      inteq_reflection [OF 2]
      inteq_reflection [OF 3]
    by auto

  show ?thesis
    unfolding inteq_reflection [OF 4] by auto
qed

lemmas enabled_controlled = inteq_reflection [OF enabled_controlled_lifted]

section Safety

text ‹The safety property of the algorithm says that termination is detected only if all nodes
are inactive. The proof works by showing that the safety invariant is actually an invariant,
and that this invariant implies the desired safety property.›

definition AllNodesInactive :: stpred where
  "AllNodesInactive ≡ PRED (∀ n. ¬ id<isNodeActive,#n>)"

definition SafetyInvariant where
  "SafetyInvariant ≡ PRED
    (∀ n. (tokenPosition < #n) ⟶ ¬ id<isNodeActive,#n>)
    ∨ (∃ n. #n ≤ tokenPosition ∧ id<nodeState,#n> = #NotTerminated)
    ∨ tokenState = #NotTerminated"

lemma safety:
  shows "⊢ Spec ⟶ □(TerminationDetected ⟶ AllNodesInactive)"
proof -
  have "⊢ Spec ⟶ □SafetyInvariant"
  proof invariant
    fix sigma
    assume s: "Spec sigma"
    thus "sigma ⊨ Init SafetyInvariant"
      by (auto simp add: Spec_def SafetyInvariant_def StartState_def Init_def)

    show "sigma ⊨ stable SafetyInvariant"
    proof (intro Stable)
      from s show "sigma ⊨ □[Next]_(isNodeActive, nodeState, tokenPosition, tokenState)"
        by (simp add: Spec_def)

      show "⊢ $SafetyInvariant ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ SafetyInvariant$"
      proof clarsimp
        fix s t
        assume s: "SafetyInvariant s"
          and st: "(s, t) ⊨ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState)"

        from st have
          "((s, t) ⊨ InitiateProbe)
           ∨ (∃n. (s, t) ⊨ PassToken n)
           ∨ (∃n. (s, t) ⊨ SendMsg n)
           ∨ (∃n. (s, t) ⊨ Deactivate n)
           ∨ ((s, t) ⊨ unchanged (isNodeActive, nodeState, tokenPosition, tokenState))"
          by (auto simp add: square_def Next_def Controlled_def Environment_def)

        thus "SafetyInvariant t"
        proof (elim disjE conjE exE)
          assume "(s, t) ⊨ unchanged (isNodeActive, nodeState, tokenPosition, tokenState)"
          with s show "SafetyInvariant t" by (simp add: SafetyInvariant_def)
        next
          assume "InitiateProbe (s, t)"
          hence step:
                "tokenPosition s = FirstNode" "tokenState s = NotTerminated ∨ nodeState s FirstNode = NotTerminated"
                "tokenPosition t = LastNode" "tokenState t = MaybeTerminated" "isNodeActive t = isNodeActive s"
                "⋀n. nodeState t n = (if n = FirstNode then MaybeTerminated else nodeState s n)"
            unfolding InitiateProbe_def updatedFun_def
            by auto

          note step_simps[simp] = `tokenPosition s = FirstNode` `tokenPosition t = LastNode` `tokenState t = MaybeTerminated` `isNodeActive t = isNodeActive s`
            `⋀n. nodeState t n = (if n = FirstNode then MaybeTerminated else nodeState s n)`

          show "SafetyInvariant t"
            unfolding SafetyInvariant_def
            apply (auto simp add: less_Node_def LastNode_def)
            by (metis Abs_Node_inverse Rep_Node Suc_pred atLeastLessThan_iff diff_Suc_less less_or_eq_imp_le neq0_conv not_less_eq)

        next
          fix n assume "Deactivate n (s, t)"
          hence step:
            "tokenPosition t = tokenPosition s" "tokenState t = tokenState s" "nodeState t = nodeState s" "⋀n. isNodeActive t n ⟹ isNodeActive s n"
            unfolding Deactivate_def updatedFun_def apply auto
            by (metis id_apply unl_before unl_con unl_lift2)

          from s show "SafetyInvariant t" by (auto simp add: less_Node_def LastNode_def SafetyInvariant_def step)

        next
          fix sender assume step: "SendMsg sender (s, t)"
          from step have step_simps[simp]: "tokenPosition t = tokenPosition s" "tokenState t = tokenState s" by (auto simp add: SendMsg_def)
          from step have n_active: "isNodeActive s sender" by (simp add: SendMsg_def)

          from step obtain receiver where receiver: "receiver ≠ sender"
            "⋀m. isNodeActive t m = (m = receiver ∨ isNodeActive s m)"
            "⋀m. nodeState t m = (if m = sender ∧ receiver > sender then NotTerminated else nodeState s m)"
            unfolding SendMsg_def updatedFun_def by auto

          show ?thesis
          proof (cases "receiver < tokenPosition s")
            case False
            with s show ?thesis
              unfolding SafetyInvariant_def less_Node_def
              apply auto
                apply (metis le_less_trans less_Node_def n_active not_le receiver(2) receiver(3))
              by (metis receiver(3))
          next
            case True
            with s receiver show ?thesis unfolding SafetyInvariant_def less_Node_def by fastforce
          qed

        next
          fix n assume step: "PassToken n (s,t)"

          hence step_tokenPosition[simp]: "tokenPosition s = n" "tokenPosition t = PreviousNode n" "n ≠ FirstNode" unfolding PassToken_def by auto

          from step have step_active[simp]: "isNodeActive t = isNodeActive s" unfolding PassToken_def by auto

          from step have step_colour: "⋀m. nodeState t m = (if m = n then MaybeTerminated else nodeState s m)"
            by (simp add: PassToken_def updatedFun_def)

          from step have step_tokenState: "tokenState t = (if nodeState s n = NotTerminated then NotTerminated else tokenState s)"
            unfolding PassToken_def by simp

          show ?thesis
          proof (cases "nodeState s n = NotTerminated ∨ tokenState s = NotTerminated")
            case True with step_tokenState show ?thesis by (auto simp add: SafetyInvariant_def)
          next
            case False
            with TerminationState.exhaust have whites: "nodeState s n = MaybeTerminated" "tokenState s = MaybeTerminated" by auto

            from whites step_colour step_tokenState have step_simps[simp]:
              "nodeState t = nodeState s" "tokenState t = tokenState s" by auto

            from step whites have n_inactive: "¬isNodeActive s n" unfolding PassToken_def by auto

            from step_tokenPosition(3)
            have gt1: "⋀m. m < n = (m < (PreviousNode n) ∨ m = PreviousNode n)"
              using Node_gt_PreviousNode not_less_iff_gr_or_eq by blast

            have gt2: "⋀m. n < m = ((PreviousNode n) < m ∧ m ≠ n)"
              using Node_gt_PreviousNode step_tokenPosition(3) by blast

            from s n_inactive show ?thesis
              unfolding SafetyInvariant_def
              apply (clarsimp simp add: gt1 gt2)
              by (metis TerminationState.simps(2) gt2 leD leI whites(1))
          qed
        qed
      qed
    qed
  qed

  moreover have "⊢ □SafetyInvariant ⟶ □(TerminationDetected ⟶ AllNodesInactive)"
    unfolding SafetyInvariant_def
  proof (intro STL4, clarsimp, intro conjI impI)
    fix w
    assume inactive_gt: "∀n. (tokenPosition w < n) ⟶ ¬ isNodeActive w n"
    show "TerminationDetected w ⟹ AllNodesInactive w"
      unfolding TerminationDetected_def AllNodesInactive_def
    proof clarsimp
      fix n assume a: "isNodeActive w n" "tokenPosition w = FirstNode" "¬ isNodeActive w FirstNode"
      with inactive_gt have "¬ n > FirstNode" by auto
      hence "n = FirstNode"
        unfolding less_Node_def FirstNode_def
        by (metis Abs_Node_inverse NodeCount_positive Rep_Node Rep_Node_inject atLeastLessThan_iff le_numeral_extra(3) nat_less_le)
      with a show False by simp
    qed
  next
    fix w
    assume "tokenState w = NotTerminated"
    thus "TerminationDetected w ⟹ AllNodesInactive w"
      unfolding TerminationDetected_def
      by auto
  next
    fix w
    assume "∃n. (n ≤ tokenPosition w) ∧ nodeState w n = NotTerminated"
    then obtain n where n: "n ≤ tokenPosition w" "nodeState w n = NotTerminated" by auto
    thus "TerminationDetected w ⟹ AllNodesInactive w"
      unfolding TerminationDetected_def AllNodesInactive_def
    proof clarsimp
      assume "tokenPosition w = FirstNode" "nodeState w FirstNode = MaybeTerminated"
      with n show False
        by (metis Abs_Node_inverse TerminationState.distinct(2) FirstNode_def NodeCount_positive Rep_Node_inverse atLeastLessThan_iff le_zero_eq less_eq_Node_def)
    qed
  qed

  ultimately show ?thesis by (simp add: Valid_def)
qed

section Liveness

text ‹When all nodes become inactive the algorithm runs through up to three further distinct
phases before detecting termination. The first phase is simply to return the token to the first
node, without any constraints on its state or the states of the nodes. The second phase
passes the token around the ring once more which sets each node's state to $MaybeTerminated$,
although the token itself may be ``contaminated'' by a $NotTerminated$ state. The third phase
passes the token around the ring one last time to remove any such contamination.›

text ‹The following predicates correspond to each step of each of these phases.›

definition AllNodesInactiveAndTokenAt where "AllNodesInactiveAndTokenAt n ≡ PRED
  (AllNodesInactive ∧ tokenPosition = #n)"

definition NodeCleaningRunAt where "NodeCleaningRunAt n ≡ PRED
  (AllNodesInactiveAndTokenAt n
  ∧ id<nodeState,#FirstNode> = #MaybeTerminated
  ∧ (∀ m. #n < #m ⟶ id<nodeState,#m> = #MaybeTerminated))"

definition TokenCleaningRunAt where "TokenCleaningRunAt n ≡ PRED
  (AllNodesInactiveAndTokenAt n
  ∧ tokenState = #MaybeTerminated
  ∧ (∀ m. id<nodeState,#m> = #MaybeTerminated))"

text ‹The liveness proof now shows that each phase completes and either detects termination
or leads to the next phase.›

lemma step:
  assumes "⊢ P ⟶ AllNodesInactive"
  assumes "⊢ P ⟶ ¬ TerminationDetected"
  assumes "⊢ $P ∧ unchanged (isNodeActive, nodeState, tokenPosition, tokenState) ⟶ P$"
  assumes "⊢ $P ∧ Controlled ⟶ Q$"
  shows   "⊢ Spec ⟶ (P ↝ Q)"
proof -
  have "⊢ (□[Next]_(isNodeActive, nodeState, tokenPosition, tokenState)
    ∧ WF(Controlled)_(isNodeActive, nodeState, tokenPosition, tokenState)) ⟶ (P ↝ Q)"
  proof (intro WF1)
    from assms have no_Environment: "⋀s t. s ⊨ P ⟹ (s, t) ⊨ Environment ⟹ False"
      by (auto simp add: Environment_def AllNodesInactive_def Valid_def SendMsg_def Deactivate_def)

    with assms
    show "⊢ $P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ P$ ∨ Q$"
      "⊢ ($P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState)) ∧ <Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ Q$"
      "⊢ $P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ $Enabled (<Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState))"
      unfolding angle_Controlled enabled_controlled Next_def square_def Valid_def AllNodesInactive_def TerminationDetected_def
        apply simp_all
        apply (meson TerminationState.exhaust, blast)
      by (metis (full_types) TerminationState.exhaust)
  qed

  thus ?thesis
    by (auto simp add: Spec_def Fairness_def)
qed

lemma liveness: "⊢ Spec ⟶ (AllNodesInactive ↝ TerminationDetected)"
proof -
  note [simp] = TokenCleaningRunAt_def NodeCleaningRunAt_def
            AllNodesInactiveAndTokenAt_def AllNodesInactive_def
            square_def Controlled_def InitiateProbe_def PassToken_def updatedFun_def
            TerminationDetected_def

  have "⊢ Spec ⟶ (AllNodesInactive ↝ AllNodesInactiveAndTokenAt FirstNode)"
  proof -
    have "⊢ AllNodesInactive = (∃n. AllNodesInactiveAndTokenAt n)" unfolding AllNodesInactiveAndTokenAt_def by auto
    hence "⊢ (AllNodesInactive ↝ AllNodesInactiveAndTokenAt FirstNode)
            = (∀n. (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt FirstNode))"
      by (metis inteq_reflection leadsto_exists)

    moreover {
      fix n
      have "⊢ Spec ⟶ (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt FirstNode)"
      proof (induct n rule: Node_induct)
        case FirstNode show ?case by (intro imp_leadsto_reflexive)
      next
        case (PreviousNode n)
        hence "⊢ Spec ⟶ (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt (PreviousNode n))"
          by (intro step, auto)
        with PreviousNode show ?case by (metis imp_leadsto_transitive)
      qed
    }

    ultimately show ?thesis by (auto simp add: Valid_def)
  qed

  moreover have "⊢ Spec ⟶ ((AllNodesInactiveAndTokenAt FirstNode ∧ ¬ TerminationDetected) ↝ NodeCleaningRunAt LastNode)"
    by (intro step, auto)

  moreover have "⋀n. ⊢ Spec ⟶ (NodeCleaningRunAt n ↝ NodeCleaningRunAt FirstNode)"
  proof -
    fix n show "?thesis n"
    proof (induct n rule: Node_induct)
      case FirstNode
      with LatticeReflexivity show ?case by auto
    next
      case (PreviousNode n)
      with Node_gt_PreviousNode Node_gt_ne
      have "⊢ Spec ⟶ (NodeCleaningRunAt n ↝ NodeCleaningRunAt (PreviousNode n))"
        by (intro step, auto)
      with PreviousNode show ?case by (metis imp_leadsto_transitive)
    qed
  qed

  moreover have "⊢ Spec ⟶ (NodeCleaningRunAt FirstNode ∧ ¬ TerminationDetected ↝ TokenCleaningRunAt LastNode)"
  proof -
    have firstNode_min: "⋀n. n = FirstNode ∨ FirstNode < n"
      using Abs_Node_inverse FirstNode_def NodeCount_positive le_less less_eq_Node_def by fastforce

    hence "⊢ NodeCleaningRunAt FirstNode
      = (AllNodesInactiveAndTokenAt FirstNode ∧ (∀ m. id<nodeState,#m> = #MaybeTerminated))"
      by (auto, force)
    thus ?thesis by (intro step, auto, metis firstNode_min)
  qed

  moreover have "⋀n. ⊢ Spec ⟶ (TokenCleaningRunAt n ↝ TerminationDetected)"
  proof -
    fix n
    show "?thesis n"
    proof (induct n rule: Node_induct)
      case FirstNode
      have "⊢ TokenCleaningRunAt FirstNode ⟶ TerminationDetected" by auto
      hence "⊢ TokenCleaningRunAt FirstNode ↝ TerminationDetected"
        using ImplLeadsto_simple by auto
      thus ?case by (auto simp add: ImplLeadsto_simple intI tempD)
    next
      case (PreviousNode n)
      hence "⊢ Spec ⟶ (TokenCleaningRunAt n ↝ TokenCleaningRunAt (PreviousNode n))"
        by (intro step, auto, blast)
      with PreviousNode show ?case by (metis imp_leadsto_transitive)
    qed
  qed

  ultimately show ?thesis
    by (metis imp_leadsto_transitive imp_leadsto_triangle_excl)
qed

end