--- a/src/HOL/UNITY/Simple/Mutex.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy Thu Jun 02 13:47:08 2005 +0200
@@ -94,13 +94,13 @@
lemma IU: "Mutex \<in> Always IU"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains)
+apply (unfold Mutex_def, safety)
done
lemma IV: "Mutex \<in> Always IV"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains)
+apply (unfold Mutex_def, safety)
done
(*The safety property: mutual exclusion*)
@@ -113,7 +113,7 @@
(*The bad invariant FAILS in V1*)
lemma "Mutex \<in> Always bad_IU"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains, auto)
+apply (unfold Mutex_def, safety, auto)
(*Resulting state: n=1, p=false, m=4, u=false.
Execution of V1 (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
@@ -127,7 +127,7 @@
(*** Progress for U ***)
lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
by (unfold Mutex_def, ensures_tac U1)
@@ -165,7 +165,7 @@
lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
by (unfold Mutex_def, ensures_tac "V1")