src/ZF/UNITY/Mutex.thy

 
 lemma Mutex_in_program [simp,TC]: "Mutex \<in> program"
 by (simp add: Mutex_def)
 
 
-method_setup constrains = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.METHOD (fn facts => 
-            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
-    "for proving safety properties"
-
-
 declare Mutex_def [THEN def_prg_Init, simp]
 ML
 {*
 program_defs_ref := [thm"Mutex_def"]
 *}

 declare  IV_def [THEN def_set_simp, simp]
 declare  bad_IU_def [THEN def_set_simp, simp]
 
 lemma IU: "Mutex \<in> Always(IU)"
 apply (rule AlwaysI, force) 
-apply (unfold Mutex_def, constrains, auto) 
+apply (unfold Mutex_def, safety, auto) 
 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*)
 lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
 apply (rule Always_weaken) 

 apply (drule_tac [2] j = x in zle_zless_trans, auto)
 done
 
 lemma "Mutex \<in> Always(bad_IU)"
 apply (rule AlwaysI, force) 
-apply (unfold Mutex_def, constrains, auto)
+apply (unfold Mutex_def, safety, auto)
 apply (subgoal_tac "#1 $<= #3")
 apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
 apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
 apply auto
 (*Resulting state: n=1, p=false, m=4, u=false.  

 
 
 (*** Progress for U ***)
 
 lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
 
 lemma U_F1:
      "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
 by (unfold Mutex_def, ensures_tac U1)
 

 
 
 (*** Progress for V ***)
 
 lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
 
 lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
 by (unfold Mutex_def, ensures_tac "V1")
 
 lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"