src/HOL/UNITY/Mutex.thy

New syntax for function update; moved to main HOL directory

(*  Title:      HOL/UNITY/Mutex.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

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

Mutex = Update + UNITY + Traces + SubstAx +

(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
syntax
  "3"       :: nat                ("3")
  "4"       :: nat                ("4")

translations
   "3"  == "Suc 2"
   "4"  == "Suc 3"


(*program variables*)
datatype pvar = PP | MM | NN | UU | VV

(*No booleans; instead True=1 and False=0*)
types state = pvar => nat

constdefs
  cmd0 :: "[pvar,pvar] => (state*state) set"
    "cmd0 u m == {(s,s'). s' = s[u:=1][m:=1] & s m = 0}"

  cmd1u :: "(state*state) set"
    "cmd1u == {(s,s'). s' = s[PP:= s VV][MM:=2] & s MM = 1}"

  cmd1v :: "(state*state) set"
    "cmd1v == {(s,s'). s' = s[PP:= 1 - s UU][NN:=2] & s NN = 1}"

  (*Put pv=0 for u's program and pv=1 for v's program*)
  cmd2 :: "[nat,pvar] => (state*state) set"
    "cmd2 pv m == {(s,s'). s' = s[m:=3] & s PP = pv & s m = 2}"

  cmd3 :: "[pvar,pvar] => (state*state) set"
    "cmd3 u m == {(s,s'). s' = s[u:=0][m:=4] & s m = 3}"

  (*Put pv=1 for u's program and pv=0 for v's program*)
  cmd4 :: "[nat,pvar] => (state*state) set"
    "cmd4 pv m == {(s,s'). s' = s[PP:=pv][m:=0] & s m = 4}"

  mutex :: "(state*state) set set"
    "mutex == {id,
	       cmd0 UU MM, cmd0 VV NN,
	       cmd1u, cmd1v,
	       cmd2 0 MM, cmd2 1 NN,
	       cmd3 UU MM, cmd3 VV NN,
	       cmd4 1 MM, cmd4 0 NN}"

  MInit :: "state set"
    "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"

  boolVars :: "state set"
    "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"

  (*Put pv=0 for u's program and pv=1 for v's program*)
  invariant :: "[nat,pvar,pvar] => state set"
    "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
			     (s m = 3 --> s PP = pv)}"

  bad_invariant :: "[nat,pvar,pvar] => state set"
    "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
			         (3 <= s m & s m <= 4 --> s PP = pv)}"


  

end