src/HOL/UNITY/Mutex.thy

--- a/src/HOL/UNITY/Mutex.thy	Thu Oct 01 18:27:55 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Thu Oct 01 18:28:18 1998 +0200
@@ -8,20 +8,10 @@
 
 Mutex = SubstAx +
 
-(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
-syntax
-  "3"       :: nat                ("3")
-  "4"       :: nat                ("4")
-
-translations
-   "3"  == "Suc 2"
-   "4"  == "Suc 3"
-
-
 record state =
   PP :: bool
-  MM :: nat
-  NN :: nat
+  MM :: int
+  NN :: int
   UU :: bool
   VV :: bool
 
@@ -30,57 +20,57 @@
   (** The program for process U **)
   
   cmd0U :: "(state*state) set"
-    "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}"
+    "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}"
 
   cmd1U :: "(state*state) set"
-    "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}"
+    "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}"
 
   cmd2U :: "(state*state) set"
-    "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}"
+    "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}"
 
   cmd3U :: "(state*state) set"
-    "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}"
+    "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}"
 
   cmd4U :: "(state*state) set"
-    "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}"
+    "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}"
 
   (** The program for process V **)
   
   cmd0V :: "(state*state) set"
-    "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}"
+    "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}"
 
   cmd1V :: "(state*state) set"
-    "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}"
+    "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}"
 
   cmd2V :: "(state*state) set"
-    "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}"
+    "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}"
 
   cmd3V :: "(state*state) set"
-    "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}"
+    "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}"
 
   cmd4V :: "(state*state) set"
-    "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}"
+    "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}"
 
   Mprg :: state program
-    "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0},
-	       Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
-	                cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
+    "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0},
+			 {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
+			  cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})"
 
 
   (** The correct invariants **)
 
   invariantU :: "state set"
-    "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
-		       (MM s = 3 --> ~ PP s)}"
+    "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
+		       (MM s = #3 --> ~ PP s)}"
 
   invariantV :: "state set"
-    "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) &
-		       (NN s = 3 --> PP s)}"
+    "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) &
+		       (NN s = #3 --> PP s)}"
 
   (** The faulty invariant (for U alone) **)
 
   bad_invariantU :: "state set"
-    "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
-		           (3 <= MM s & MM s <= 4 --> ~ PP s)}"
+    "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) &
+		           (#3 <= MM s & MM s <= #4 --> ~ PP s)}"
 
 end