now trans_tac is part of the claset...

--- a/src/HOL/UNITY/Handshake.ML	Fri Aug 14 12:06:34 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Fri Aug 14 13:52:42 1998 +0200
@@ -50,7 +50,6 @@
 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
     GreaterThan_bounded_induct 1);
 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-by (trans_tac 2);
 (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
 by (rtac LeadsTo_Diff 1);
 by (rtac lemma2_2 2);

--- a/src/HOL/UNITY/LessThan.ML	Fri Aug 14 12:06:34 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Fri Aug 14 13:52:42 1998 +0200
@@ -7,6 +7,9 @@
 *)
 
 
+claset_ref() := claset() addaltern ("trans_tac",trans_tac);
+
+
 (*** lessThan ***)
 
 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";

--- a/src/HOL/UNITY/Lift.ML	Fri Aug 14 12:06:34 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Fri Aug 14 13:52:42 1998 +0200
@@ -33,10 +33,18 @@
 	  moving_up_def, moving_down_def];
 
 
+val nat_exhaust_less_pred = 
+    read_instantiate_sg (sign_of thy) [("P", "?m < ?y-1")] nat.exhaust;
+
+val nat_exhaust_le_pred = 
+    read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
+
+val nat_exhaust_pred_le = 
+    read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
+
 Goal "0 < n ==> (m <= n-1) = (m<n)";
 by (exhaust_tac "n" 1);
 by Auto_tac;
-by (REPEAT_FIRST trans_tac);
 qed "le_pred_eq";
 
 Goal "m < n ==> m <= n-1";
@@ -82,57 +90,44 @@
 qed "moving_down";
 
 
-xxxxxxxxxxxxxxxx;
-
-Goalw [Lprg_def] "Invariant Lprg bounded";
+Goal "Invariant Lprg bounded";
 by (rtac InvariantI 1);
+br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
+bw Lprg_def;
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
-by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq])));
-by (REPEAT_FIRST trans_tac);
-by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
-by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
-by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
+by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
+by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
+by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]));
 qed "bounded";
 
-Goalw [Lprg_def] "Invariant Lprg invariantV";
-by (rtac InvariantI 1);
-by (constrains_tac cmd_defs 2);
-by Auto_tac;
-qed "invariantV";
+
 
-val invariantUV = invariant_Int_rule [invariantU, invariantV];
+(*** Progress ***)
 
 
-(*The safety property: mutual exclusion*)
-Goal "(reachable Lprg) Int {s. MM s = 3 & NN s = 3} = {}";
-by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
-by Auto_tac;
-qed "mutual_exclusion";
+val abbrev_defs = [moving_def, stopped_def, 
+		   opened_def, closed_def, atFloor_def];
 
+val defs = cmd_defs@always_defs@abbrev_defs;
 
-(*** Progress for U ***)
+(***
 
-Goalw [unless_def] "unless (Acts Lprg) {s. MM s=2} {s. MM s=3}";
-by (constrains_tac cmd_defs 1);
-qed "U_F0";
-
-Goal "LeadsTo Lprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
-by (ensures_tac cmd_defs "cmd1U" 1);
+Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
+by (ensures_tac defs "open_act" 1);
 qed "U_F1";
 
 Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
 by (cut_facts_tac [invariantUV] 1);
 by (rewtac Lprg_def);
-by (ensures_tac cmd_defs "cmd2U" 1);
+by (ensures_tac defs "cmd2U" 1);
 qed "U_F2";
 
 Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
 by (rtac leadsTo_imp_LeadsTo 1); 
 by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
-by (ensures_tac cmd_defs "cmd4U" 2);
-by (ensures_tac cmd_defs "cmd3U" 1);
+by (ensures_tac defs "cmd4U" 2);
+by (ensures_tac defs "cmd3U" 1);
 qed "U_F3";
 
 Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
@@ -142,3 +137,4 @@
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val U_lemma2 = result();
 
+***)

--- a/src/HOL/UNITY/Lift.thy	Fri Aug 14 12:06:34 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy	Fri Aug 14 13:52:42 1998 +0200
@@ -27,25 +27,44 @@
   
   (** Abbreviations: the "always" part **)
   
-  above :: "state set"
+  above :: state set
     "above == {s. EX i. floor s < i & i <= max & i : req s}"
 
-  below :: "state set"
+  below :: state set
     "below == {s. EX i. min <= i & i < floor s & i : req s}"
 
-  queueing :: "state set"
+  queueing :: state set
     "queueing == above Un below"
 
-  goingup :: "state set"
+  goingup :: state set
     "goingup == above Int ({s. up s} Un Compl below)"
 
-  goingdown :: "state set"
+  goingdown :: state set
     "goingdown == below Int ({s. ~ up s} Un Compl above)"
 
-  ready :: "state set"
+  ready :: state set
     "ready == {s. stop s & ~ open s & move s}"
 
+ 
+  (** Further abbreviations **)
 
+  moving :: state set
+    "moving ==  {s. ~ stop s & ~ open s}"
+
+  stopped :: state set
+    "stopped == {s. stop s  & ~ open s &  move s}"
+
+  opened :: state set
+    "opened ==  {s. stop s  &  open s  &  move s}"
+
+  closed :: state set
+    "closed ==  {s. stop s  & ~ open s &  move s}"
+
+  atFloor :: nat => state set
+    "atFloor n ==  {s. floor s = n}"
+
+
+  
   (** The program **)
   
   request_act :: "(state*state) set"
@@ -99,11 +118,6 @@
   bounded :: state set
     "bounded == {s. min <= floor s & floor s <= max}"
 
-  (** ???
-		    (~ stop s & up s --> floor s < max) &
-		    (~ stop s & ~ up s --> min < floor s)}"
-  **)
-
   open_stop :: state set
     "open_stop == {s. open s --> stop s}"
   
@@ -121,7 +135,8 @@
     "moving_down == {s. ~ stop s & ~ up s -->
                      (EX f. min <= f & f <= floor s & f : req s)}"
   
-  valid :: "state set"
+  (*intersection of all invariants: NECESSARY??*)
+  valid :: state set
     "valid == bounded Int open_stop Int open_move"
 
 end

--- a/src/HOL/UNITY/Mutex.ML	Fri Aug 14 12:06:34 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Fri Aug 14 13:52:42 1998 +0200
@@ -56,7 +56,6 @@
 by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac cmd_defs 1);
-by (REPEAT (trans_tac 1));
 by (safe_tac (claset() addSEs [le_SucE]));
 by (Asm_full_simp_tac 1);
 (*Resulting state: n=1, p=false, m=4, u=false.