# HG changeset patch
# User paulson
# Date 926067720 -7200
# Node ID f72f560af0a198cfc024f7ea8715863684a8b836
# Parent  2d47dee036b536ef34973777509f20749224bbc7
tidied

diff -r 2d47dee036b5 -r f72f560af0a1 src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Fri May 07 10:50:28 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Fri May 07 11:02:00 1999 +0200
@@ -45,15 +45,7 @@
 Goal "Mutex : Always bad_IU";
 by (rtac AlwaysI 1);
 by (constrains_tac 2);
-by (Force_tac 1);
-(*Needs a decision procedure to simplify the resulting state*)
-by (auto_tac (claset(), 
-	      simpset_of Int.thy addsimps
-	        [zadd_int, integ_of_Pls, integ_of_Min, 
-		 integ_of_BIT, le_int_Suc_eq]));
-by (dtac zle_trans 1 THEN assume_tac 1);
-by (full_simp_tac (simpset_of Int.thy) 1);
-by (asm_full_simp_tac (simpset() addsimps int_simps) 1);
+by Auto_tac;
 (*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!*)
@@ -62,10 +54,7 @@
 
 
 Goal "(#1 <= i & i <= #3) = (i = #1 | i = #2 | i = #3)";
-by (auto_tac (claset(),
-	      simpset_of Int.thy addsimps
-	        [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, 
-		 integ_of_BIT]));
+by (arith_tac 1);
 qed "eq_123";
 
 
@@ -165,27 +154,24 @@
 
 (*Misra's F6*)
 Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}";
-by (rtac LeadsTo_Un_duplicate 1);
-by (rtac LeadsTo_cancel2 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
 by (rtac U_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
 by (stac Un_commute 1);
-by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
+by Auto_tac;
 qed "m1_Leadsto_3";
 
-
 (*The same for V*)
 Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}";
-by (rtac LeadsTo_Un_duplicate 1);
-by (rtac LeadsTo_cancel2 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
 by (rtac V_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
 by (stac Un_commute 1);
-by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless  RSN(2, LeadsTo_cancel2)) 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
+by Auto_tac;
 qed "n1_Leadsto_3";