src/ZF/UNITY/Mutex.thy

val local_imp_def = thm "induct_implies_def";

(*  Title:      ZF/UNITY/Mutex.thy
    ID:         $Id$
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra

Variables' types are introduced globally so that type verification of
UNITY programs/specifications reduce to the usual ZF typechecking.
An ill-tyed expression will reduce to the empty set.
*)

Mutex = SubstAx + 
consts
  p, m, n, u, v :: i
  
translations
  "p" == "Var([])"
  "m" == "Var([0])"
  "n" == "Var([1])"
  "u" == "Var([1,0])"
  "v" == "Var([1,1])"
  
rules (** Type declarations  **)
  p_type  "type_of(p)=bool"
  m_type  "type_of(m)=int"
  n_type  "type_of(n)=int"
  u_type  "type_of(u)=bool"
  v_type  "type_of(v)=bool"
  
constdefs
  (** The program for process U **)
   U0 :: i
    "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"

  U1 :: i
  "U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) &  s`m = #1}"

  U2 :: i
    "U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}"

  U3 :: i
    "U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}"

  U4 :: i
    "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"

  
   (** The program for process V **)
  
  V0 :: i
    "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"

  V1 :: i
    "V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}"

  V2 :: i
    "V2 == {<s,t>:state*state. t  = s(n:=#3) & s`p=1 & s`n = #2}"

  V3 :: i
  "V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}"

  V4 :: i
    "V4 == {<s,t>:state*state. t  = s (p:=0, n:=#0) & s`n = #4}"

 Mutex :: i
 "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0},
                       {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, action)"

  (** The correct invariants **)

  IU :: i
    "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))
	             & (s`m = #3 --> s`p=0)}"

  IV :: i
    "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))
	              & (s`n = #3 --> s`p=1)}"

  (** The faulty invariant (for U alone) **)

  bad_IU :: i
    "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m  $<= #3))&
                   (#3 $<= s`m & s`m $<= #4 --> s`p=0)}"

end