Theory Token

(*  Title:      HOL/UNITY/Simple/Token.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)


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 (auto simp add: not_E_eq)
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 (cases ‹i < j›)
   apply (auto simp add: nodeOrder_def next_def mod_Suc add.commute [of _ N])
  apply (simp only: diff_add_assoc mod_add_self1)
  apply simp
  done

text‹From "A Logic for Concurrent Programming", but not used in Chapter 4.
  Note the use of ‹cases›.  Reasoning about leadsTo takes practice!›
lemma TR7_nodeOrder:
     "[| i<N; j<N |] ==>    
      F ∈ (HasTok i) leadsTo ({s. (token s, i) ∈ nodeOrder j} ∪ HasTok j)"
apply (cases "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 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 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 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 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

end