# Theory Token

Up to index of Isabelle/HOL/UNITY

theory Token
imports WFair
begin

    (*  Title:      HOL/UNITY/Token
        ID:         $Id: Token.thy,v 1.4 2005/03/23 11:08:27 paulson Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge
    *)

    header {*The Token Ring*}

    theory Token
    imports "../WFair"

    begin

    text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*}

    subsection{*Definitions*}

    datatype pstate = Hungry | Eating | Thinking
        --{*process states*}

    record state =
      token :: "nat"
      proc  :: "nat => pstate"

    constdefs
      HasTok :: "nat => state set"
        "HasTok i == {s. token s = i}"

      H :: "nat => state set"
        "H i == {s. proc s i = Hungry}"

      E :: "nat => state set"
        "E i == {s. proc s i = Eating}"

      T :: "nat => state set"
        "T i == {s. proc s i = Thinking}"

    locale Token =
      fixes N and F and nodeOrder and "next"
      defines nodeOrder_def:
           "nodeOrder j == measure(%i. ((j+N)-i) mod N) ∩ {..<N} × {..<N}"
          and next_def:
           "next i == (Suc i) mod N"
      assumes N_positive [iff]: "0<N"
          and TR2:  "F ∈ (T i) co (T i ∪ H i)"
          and TR3:  "F ∈ (H i) co (H i ∪ E i)"
          and TR4:  "F ∈ (H i - HasTok i) co (H i)"
          and TR5:  "F ∈ (HasTok i) co (HasTok i ∪ -(E i))"
          and TR6:  "F ∈ (H i ∩ HasTok i) leadsTo (E i)"
          and TR7:  "F ∈ (HasTok i) leadsTo (HasTok (next i))"

    lemma HasToK_partition: "[| s ∈ HasTok i; s ∈ HasTok j |] ==> i=j"
    by (unfold HasTok_def, auto)

    lemma not_E_eq: "(s ∉ E i) = (s ∈ H i | s ∈ T i)"
    apply (simp add: H_def E_def T_def)
    apply (case_tac "proc s i", auto)
    done

    lemma (in Token) token_stable: "F ∈ stable (-(E i) ∪ (HasTok i))"
    apply (unfold stable_def)
    apply (rule constrains_weaken)
    apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
    apply (auto simp add: not_E_eq)
    apply (simp_all add: H_def E_def T_def)
    done

    subsection{*Progress under Weak Fairness*}

    lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
    apply (unfold nodeOrder_def)
    apply (rule wf_measure [THEN wf_subset], blast)
    done

    lemma (in Token) nodeOrder_eq:
         "[| i<N; j<N |] ==> ((next i, i) ∈ nodeOrder j) = (i ≠ j)"
    apply (unfold nodeOrder_def next_def measure_def inv_image_def)
    apply (auto simp add: mod_Suc mod_geq)
    apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
    done

    text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
      Note the use of @{text case_tac}.  Reasoning about leadsTo takes practice!*}
    lemma (in Token) TR7_nodeOrder:
         "[| i<N; j<N |] ==>
          F ∈ (HasTok i) leadsTo ({s. (token s, i) ∈ nodeOrder j} ∪ HasTok j)"
    apply (case_tac "i=j")
    apply (blast intro: subset_imp_leadsTo)
    apply (rule TR7 [THEN leadsTo_weaken_R])
    apply (auto simp add: HasTok_def nodeOrder_eq)
    done

    text{*Chapter 4 variant, the one actually used below.*}
    lemma (in Token) TR7_aux: "[| i<N; j<N; i≠j |]
          ==> F ∈ (HasTok i) leadsTo {s. (token s, i) ∈ nodeOrder j}"
    apply (rule TR7 [THEN leadsTo_weaken_R])
    apply (auto simp add: HasTok_def nodeOrder_eq)
    done

    lemma (in Token) token_lemma:
         "({s. token s < N} ∩ token -` {m}) = (if m<N then token -` {m} else {})"
    by auto

    text{*Misra's TR9: the token reaches an arbitrary node*}
    lemma  (in Token) leadsTo_j: "j<N ==> F ∈ {s. token s < N} leadsTo (HasTok j)"
    apply (rule leadsTo_weaken_R)
    apply (rule_tac I = "-{j}" and f = token and B = "{}"
           in wf_nodeOrder [THEN bounded_induct])
    apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
     prefer 2 apply blast
    apply clarify
    apply (rule TR7_aux [THEN leadsTo_weaken])
    apply (auto simp add: HasTok_def nodeOrder_def)
    done

    text{*Misra's TR8: a hungry process eventually eats*}
    lemma (in Token) token_progress:
         "j<N ==> F ∈ ({s. token s < N} ∩ H j) leadsTo (E j)"
    apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
    apply (rule_tac [2] TR6)
    apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
    done

    end

### Definitions

lemma HasToK_partition:

      [| s ∈ HasTok i; s ∈ HasTok j |] ==> i = j

lemma not_E_eq:

      (s ∉ E i) = (s ∈ H i ∨ s ∈ T i)

lemma token_stable:

      Token N F ==> F ∈ stable (- E i ∪ HasTok i)

### Progress under Weak Fairness

lemma wf_nodeOrder:

      Token N F ==> wf (measure (%i. (j + N - i) mod N) ∩ {..<N} × {..<N})

lemma nodeOrder_eq:

      [| Token N F; i < N; j < N |]
      ==> ((Suc i mod N, i) ∈ measure (%i. (j + N - i) mod N) ∩ {..<N} × {..<N}) =
          (i ≠ j)

lemma TR7_nodeOrder:

      [| Token N F; i < N; j < N |]
      ==> F ∈ HasTok i leadsTo
              {s. (token s, i) ∈ measure (%i. (j + N - i) mod N) ∩ {..<N} × {..<N}} ∪
              HasTok j

lemma TR7_aux:

      [| Token N F; i < N; j < N; i ≠ j |]
      ==> F ∈ HasTok i leadsTo
              {s. (token s, i) ∈ measure (%i. (j + N - i) mod N) ∩ {..<N} × {..<N}}

lemma token_lemma:

      Token N F
      ==> {s. token s < N} ∩ token -` {m} = (if m < N then token -` {m} else {})

lemma leadsTo_j:

      [| Token N F; j < N |] ==> F ∈ {s. token s < N} leadsTo HasTok j

lemma token_progress:

      [| Token N F; j < N |] ==> F ∈ {s. token s < N} ∩ H j leadsTo E j