src/HOL/UNITY/Simple/Mutex.thy
changeset 11868 56db9f3a6b3e
parent 11704 3c50a2cd6f00
child 13785 e2fcd88be55d
     1.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4    (** The program for process U **)
     1.5    
     1.6    U0 :: command
     1.7 -    "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}"
     1.8 +    "U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}"
     1.9  
    1.10    U1 :: command
    1.11 -    "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}"
    1.12 +    "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}"
    1.13  
    1.14    U2 :: command
    1.15      "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
    1.16 @@ -34,15 +34,15 @@
    1.17      "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
    1.18  
    1.19    U4 :: command
    1.20 -    "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}"
    1.21 +    "U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}"
    1.22  
    1.23    (** The program for process V **)
    1.24    
    1.25    V0 :: command
    1.26 -    "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}"
    1.27 +    "V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}"
    1.28  
    1.29    V1 :: command
    1.30 -    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}"
    1.31 +    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}"
    1.32  
    1.33    V2 :: command
    1.34      "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
    1.35 @@ -51,10 +51,10 @@
    1.36      "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
    1.37  
    1.38    V4 :: command
    1.39 -    "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}"
    1.40 +    "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
    1.41  
    1.42    Mutex :: state program
    1.43 -    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0},
    1.44 +    "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
    1.45  		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    1.46  			  UNIV)"
    1.47  
    1.48 @@ -62,15 +62,15 @@
    1.49    (** The correct invariants **)
    1.50  
    1.51    IU :: state set
    1.52 -    "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
    1.53 +    "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
    1.54  
    1.55    IV :: state set
    1.56 -    "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
    1.57 +    "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
    1.58  
    1.59    (** The faulty invariant (for U alone) **)
    1.60  
    1.61    bad_IU :: state set
    1.62 -    "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) &
    1.63 +    "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
    1.64  	           (3 <= m s & m s <= 4 --> ~ p s)}"
    1.65  
    1.66  end