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