Theory Token

theory Token
imports WFair
```(*  Title:      HOL/UNITY/Simple/Token.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹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"

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

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

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

definition T :: "nat => state set" where
"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 (cases "proc s i", auto)
done

context Token
begin

lemma 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 (simp_all add: H_def E_def T_def)
done

subsection‹Progress under Weak Fairness›

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

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

text‹From "A Logic for Concurrent Programming", but not used in Chapter 4.
lemma TR7_nodeOrder:
"[| i<N; j<N |] ==>
F ∈ (HasTok i) leadsTo ({s. (token s, i) ∈ nodeOrder j} ∪ HasTok j)"
apply (cases "i=j")
apply (auto simp add: HasTok_def nodeOrder_eq)
done

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

lemma 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 leadsTo_j: "j<N ==> F ∈ {s. token s < N} leadsTo (HasTok j)"
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 (auto simp add: HasTok_def nodeOrder_def)
done

text‹Misra's TR8: a hungry process eventually eats›
lemma token_progress:
"j<N ==> F ∈ ({s. token s < N} ∩ H j) leadsTo (E j)"