# HG changeset patch
# User paulson
# Date 903515671 -7200
# Node ID d75c03cf77b5d745b86a04e7041b5fc1848010b1
# Parent  22c195854229e0f8c572ff7fa4a189a3114c8cfb
Misc changes

diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -9,6 +9,10 @@
 
 (*** Constrains ***)
 
+(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*)
+Blast.overloaded ("Constrains.Constrains", 
+		  HOLogic.dest_setT o domain_type o range_type);
+
 (*constrains (Acts prg) B B'
   ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
 bind_thm ("constrains_reachable_Int",
@@ -80,7 +84,8 @@
     "[| ALL i:I. Constrains prg (A i) (A' i) |]   \
 \    ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
 by (dtac ball_constrains_INT 1);
-by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
+by (dtac constrains_reachable_Int 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "ball_Constrains_INT";
 
 Goalw [Constrains_def]
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -32,13 +32,14 @@
 by (constrains_tac [prgF_def,cmdF_def] 1);
 qed "invFG";
 
-Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
+Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
+\                              ({s. NF s = k} Int {s. BB s})";
 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
 by (constrains_tac [prgF_def,cmdF_def] 1);
 qed "lemma2_1";
 
-Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
+Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (constrains_tac [prgG_def,cmdG_def] 2);
 by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
@@ -55,6 +56,6 @@
 by (rtac lemma2_2 2);
 by (rtac LeadsTo_Trans 1);
 by (rtac lemma2_2 2);
-by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
+by (rtac (lemma2_1) 1);
 by Auto_tac;
 qed "progress";
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -6,6 +6,13 @@
 The Lift-Control Example
 *)
 
+(*ARITH.ML??*)
+Goal "m-1 < n ==> m <= n";
+by (exhaust_tac "m" 1);
+by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
+qed "pred_less_imp_le";
+
+
 val always_defs = [above_def, below_def, queueing_def, 
 		   goingup_def, goingdown_def, ready_def];
 
@@ -13,8 +20,6 @@
 		request_act_def, open_act_def, close_act_def,
 		req_up_act_def, req_down_act_def, move_up_def, move_down_def];
 
-AddIffs [min_le_max];
-
 Goalw [Lprg_def] "id : Acts Lprg";
 by (Simp_tac 1);
 qed "id_in_Acts";
@@ -32,9 +37,8 @@
 Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
 	  moving_up_def, moving_down_def];
 
+AddIffs [min_le_max];
 
-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;
@@ -47,6 +51,11 @@
 by Auto_tac;
 qed "le_pred_eq";
 
+Goal "0 < n ==> (m-1 < n) = (m<=n)";
+by (exhaust_tac "m" 1);
+by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
+qed "less_pred_eq";
+
 Goal "m < n ==> m <= n-1";
 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
 qed "less_imp_le_pred";
@@ -107,34 +116,303 @@
 
 
 val abbrev_defs = [moving_def, stopped_def, 
-		   opened_def, closed_def, atFloor_def];
+		   opened_def, closed_def, atFloor_def, Req_def];
 
 val defs = cmd_defs@always_defs@abbrev_defs;
 
-(***
+
+(** The HUG'93 paper mistakenly omits the Req n from these! **)
 
 Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
 by (ensures_tac defs "open_act" 1);
-qed "U_F1";
+qed "E_thm01";
+
+Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
+\                  (Req n Int opened - atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
+by (ensures_tac defs "open_act" 1);
+qed "E_thm02";
+
+Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
+\                  (Req n Int closed - (atFloor n - queueing))";
+by (ensures_tac defs "close_act" 1);
+qed "E_thm03";
+
+Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
+\                  (opened Int atFloor n)";
+by (ensures_tac defs "open_act" 1);
+qed "E_thm04";
+
+
+(** Theorem 5.  Statements of thm05a and thm05b were wrong! **)
+
+Open_locale "floor"; 
+
+AddIffs [thm "min_le_n", thm "n_le_max"];
+
+(*NOT an ensures property, but a mere inclusion*)
+Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
+\                  ((closed Int goingup Int Req n)  Un \
+\                   (closed Int goingdown Int Req n))";
+br subset_imp_LeadsTo 1;
+by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
+qed "E_thm05c";
+
+Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
+\                  (moving Int Req n)";
+br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
+by (ensures_tac defs "req_down_act" 2);
+by (ensures_tac defs "req_up_act" 1);
+qed "lift_2";
+
+
+
+val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
+and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
+(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
+
+val [lift_3] = 
+goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
+br LeadsTo_Trans 1;
+br (E_thm04 RS LeadsTo_Un) 2;
+br LeadsTo_Un_post' 2;
+br (E_thm01 RS LeadsTo_Trans_Un') 2;
+br (lift_3 RS LeadsTo_Trans_Un') 2;
+br (lift_2 RS LeadsTo_Trans_Un') 2;
+br (E_thm03 RS LeadsTo_Trans_Un') 2;
+br E_thm02 2;
+br (open_move RS Invariant_LeadsToI) 1;
+br (open_stop RS Invariant_LeadsToI) 1;
+br subset_imp_LeadsTo 1;
+by (rtac id_in_Acts 2);
+bws defs;
+by (Clarify_tac 1);
+	(*stops simplification from looping*)
+by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
+by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
+qed "lift_1";
+
 
-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 defs "cmd2U" 1);
-qed "U_F2";
+val rev_mp' = read_instantiate_sg (sign_of thy) 
+                 [("P", "0 < metric ?n ?s")] rev_mp;
+
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
+\                  (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_up_act" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+by (auto_tac (claset() addIs [diff_Suc_less_diff], 
+	      simpset() addsimps [arith1, arith2, metric_def]));
+qed "E_thm16a";
+
+
+(*arith1 comes from
+ 1. !!s i.
+       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
+          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
+          ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
+          Suc (floor s) < n; 0 < floor s - min |]
+       ==> n - Suc (floor s) < floor s - min + (n - min)
+*)
+
+(*arith2 comes from
+ 2. !!s i.
+       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
+          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
+          ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
+          Suc (floor s) < n; min < n |]
+       ==> n - Suc (floor s) < floor s - min + (n - min)
+*)
+
+
+xxxxxxxxxxxxxxxx;
+
+Goal "j<=i ==> i - j < Suc i - j";
+by (REPEAT (etac rev_mp 1));
+by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
+by Auto_tac;
+qed "diff_less_Suc_diff";
+
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
+\                  (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_down_act" 1);
+be rev_mp 2;
+be rev_mp 1;
+by (dtac less_eq_Suc_add 2);
+by (Clarify_tac 2);
+by (Asm_full_simp_tac 2);
+by (dtac less_eq_Suc_add 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+
+by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
+by (REPEAT (Safe_step_tac 1));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
+by (REPEAT (Safe_step_tac 1));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
+by (REPEAT (Safe_step_tac 1));
+
+
+
+
+
+
+
+Goal "[| i + k < n;  Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
+by (REPEAT (etac rev_mp 1));
+by (arith_oracle_tac 1);
+
 
-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 defs "cmd4U" 2);
-by (ensures_tac defs "cmd3U" 1);
-qed "U_F3";
+by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(blast_tac (claset() addEs [less_asym]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+
+
+by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
+
+
+by (REPEAT (Safe_step_tac 2));
+by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
+
+by (auto_tac (claset() addIs [diff_Suc_less_diff], 
+	      simpset() addsimps [metric_def]));
+qed "E_thm16b";
+
+
+
+Goal "[|  m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
+
+
+not_less_iff_le
+
+Goal "[|  ~ m < n; m - 1 < n |] ==> n = m";
+by (cut_facts_tac [less_linear] 1);
+by (blast_tac (claset() addSEs [less_irrefl]) 1);
+ by (REPEAT (etac rev_mp 1));
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (arith_oracle_tac 1);
+
+
+
+
+
+
+
+(**in the postscript file, but too horrible**)
+
+Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
+\                  (moving Int Req n Int {s. metric n s < N})";
+by (ensures_tac defs "req_down_act" 1);
+by (REPEAT_FIRST (etac rev_mp'));
+
+by (dtac less_eq_Suc_add 2);
+by (Clarify_tac 2);
+by (Asm_full_simp_tac 2);
+by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
+
+
+yyyyyyyyyyyyyyyy;
+
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(Blast_tac 2);
+by(Blast_tac 2);
+by (REPEAT (Safe_step_tac 2));
+by(blast_tac (claset() addEs [less_asym]) 2);
+by(blast_tac (claset() addDs [le_anti_sym]
+		       addSDs [leI, pred_less_imp_le]) 2);
+by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
+
 
-Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
-	  MRS LeadsTo_Diff) 1);
-by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
-val U_lemma2 = result();
+by(Blast_tac 3);
+
+
+
+
+
+
+
+Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
+fe rev_mp;
+by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
+		by (ALLGOALS Asm_simp_tac);
+
+by (arith_oracle_tac 1);
+
+
+Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
+by (REPEAT (etac rev_mp 1));
+by (arith_oracle_tac 1);
+
+
+
+
+
+
+
+infixr TRANS;
+fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
+
+E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
+
+
+
+[E_thm02, 
+ E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
+
 
-***)
+val sact = "open_act";
+val sact = "move_up_act";
+
+val (main_def::CDEFS) = defs;
+
+by (REPEAT (Invariant_Int_tac 1));
+
+by (etac Invariant_LeadsTo_Basis 1 
+	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
+		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1));
+
+by (res_inst_tac [("act", sact)] transient_mem 2);
+by (simp_tac (simpset() addsimps (Domain_partial_func::CDEFS)) 3);
+by (force_tac (claset(), simpset() addsimps [main_def]) 2);
+by (constrains_tac (main_def::CDEFS) 1);
+by (rewrite_goals_tac CDEFS);
+by (ALLGOALS Clarify_tac);
+by (Auto_tac);
+
+by(Force_tac 2);
+
+
+
+yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
+
+
+
+Goalw [transient_def]
+     "transient acts A = (EX act:acts. A <= act^-1 ^^ (Compl A))";
+by Safe_tac;
+by (ALLGOALS (rtac bexI));
+by (TRYALL assume_tac);
+by (Blast_tac 1);
+br conjI 1;
+by (Blast_tac 1);
+(*remains to show  
+  [| act : acts; A <= act^-1 ^^ Compl A |] ==> act ^^ A <= Compl A
+*)
+
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy	Wed Aug 19 10:34:31 1998 +0200
@@ -4,6 +4,8 @@
     Copyright   1998  University of Cambridge
 
 The Lift-Control Example
+
+
 *)
 
 Lift = SubstAx +
@@ -17,11 +19,15 @@
   move  :: bool		(*whether moving takes precedence over opening*)
 
 consts
-  min, max :: nat	(*least and greatest floors*)
+  min, max :: nat       (*least and greatest floors*)
 
 rules
   min_le_max  "min <= max"
   
+  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
+  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
+  arith2      "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
+
 
 constdefs
   
@@ -37,7 +43,7 @@
     "queueing == above Un below"
 
   goingup :: state set
-    "goingup == above Int ({s. up s} Un Compl below)"
+    "goingup   == above Int  ({s. up s}  Un Compl below)"
 
   goingdown :: state set
     "goingdown == below Int ({s. ~ up s} Un Compl above)"
@@ -52,17 +58,20 @@
     "moving ==  {s. ~ stop s & ~ open s}"
 
   stopped :: state set
-    "stopped == {s. stop s  & ~ open s &  move s}"
+    "stopped == {s. stop s  & ~ open s & ~ move s}"
 
   opened :: state set
     "opened ==  {s. stop s  &  open s  &  move s}"
 
-  closed :: state set
+  closed :: state set  (*but this is the same as ready!!*)
     "closed ==  {s. stop s  & ~ open s &  move s}"
 
   atFloor :: nat => state set
     "atFloor n ==  {s. floor s = n}"
 
+  Req :: nat => state set
+    "Req n ==  {s. n : req s}"
+
 
   
   (** The program **)
@@ -125,7 +134,7 @@
     "open_move == {s. open s --> move s}"
   
   stop_floor :: state set
-    "stop_floor == {s. open s & ~ move s --> floor s : req s}"
+    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
   
   moving_up :: state set
     "moving_up == {s. ~ stop s & up s -->
@@ -135,8 +144,19 @@
     "moving_down == {s. ~ stop s & ~ up s -->
                      (EX f. min <= f & f <= floor s & f : req s)}"
   
-  (*intersection of all invariants: NECESSARY??*)
-  valid :: state set
-    "valid == bounded Int open_stop Int open_move"
+  metric :: [nat,state] => nat
+    "metric n s == if up s & floor s < n then n - floor s
+		   else if ~ up s & n < floor s then floor s - n
+		   else if up s & n < floor s then (max - floor s) + (max-n)
+		   else if ~ up s & floor s < n then (floor s - min) + (n-min)
+		   else 0"
+
+locale floor =
+  fixes 
+    n	:: nat
+  assumes
+    min_le_n    "min <= n"
+    n_le_max    "n <= max"
+  defines
 
 end
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -76,7 +76,7 @@
 qed "U_F1";
 
 Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
-by (cut_facts_tac [invariantUV] 1);
+by (cut_facts_tac [invariantU] 1);
 by (rewtac Mprg_def);
 by (ensures_tac cmd_defs "cmd2U" 1);
 qed "U_F2";
@@ -88,7 +88,7 @@
 qed "U_F3";
 
 Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
@@ -125,7 +125,7 @@
 qed "V_F1";
 
 Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
-by (cut_facts_tac [invariantUV] 1);
+by (cut_facts_tac [invariantV] 1);
 by (ensures_tac cmd_defs "cmd2V" 1);
 qed "V_F2";
 
@@ -136,7 +136,7 @@
 qed "V_F3";
 
 Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
-by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -6,6 +6,9 @@
 LeadsTo relation, restricted to the set of reachable states.
 *)
 
+(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*)
+Blast.overloaded ("SubstAx.LeadsTo", 
+		  HOLogic.dest_setT o domain_type o range_type);
 
 
 (*** Specialized laws for handling invariants ***)
@@ -42,7 +45,7 @@
 by (Simp_tac 1);
 by (stac Int_Union 1);
 by (blast_tac (claset() addIs [leadsTo_UN,
-			        simplify (simpset()) prem]) 1);
+			       simplify (simpset()) prem]) 1);
 qed "LeadsTo_Union";
 
 
@@ -88,15 +91,36 @@
 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
 qed_spec_mp "LeadsTo_weaken_R";
 
-
 Goal "[| LeadsTo prg A A';  B <= A; id: Acts prg |]  \
 \     ==> LeadsTo prg B A'";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
 qed_spec_mp "LeadsTo_weaken_L";
 
+Goal "[| LeadsTo prg A A'; id: Acts prg;   \
+\        B  <= A;   A' <= B' |] \
+\     ==> LeadsTo prg B B'";
+(*PROOF FAILED unless the Trans rule is last*)
+by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
+			       LeadsTo_Trans]) 1);
+qed "LeadsTo_weaken";
 
-(*Distributes over binary unions*)
+
+(** Two theorems for "proof lattices" **)
+
+Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
+qed "LeadsTo_Un_post";
+
+Goal "[| id: Acts prg;  LeadsTo prg A B;  LeadsTo prg B C |] \
+\     ==> LeadsTo prg (A Un B) C";
+by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
+			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
+qed "LeadsTo_Trans_Un";
+
+
+(** Distributive laws **)
+
 Goal "id: Acts prg ==> \
 \       LeadsTo prg (A Un B) C  =  \
 \       (LeadsTo prg A C & LeadsTo prg B C)";
@@ -116,15 +140,6 @@
 qed "LeadsTo_Union_distrib";
 
 
-Goal "[| LeadsTo prg A A'; id: Acts prg;   \
-\        B  <= A;   A' <= B' |] \
-\     ==> LeadsTo prg B B'";
-(*PROOF FAILED*)
-by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
-			       LeadsTo_weaken_L]) 1);
-qed "LeadsTo_weaken";
-
-
 (** More rules using the premise "Invariant prg" **)
 
 Goalw [LeadsTo_def, Constrains_def]
@@ -160,12 +175,18 @@
 
 (*Set difference: maybe combine with leadsTo_weaken_L??
   This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: Acts prg |] \
+Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
 \     ==> LeadsTo prg A C";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
+by (stac (Un_Diff_Int RS sym) 1 THEN rtac LeadsTo_Un 1);
+by (REPEAT (assume_tac 1));
+(*One step, but PROOF FAILED...
+  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
+*)
 qed "LeadsTo_Diff";
 
 
+
+
 val prems = 
 Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
 \     ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
@@ -405,8 +426,10 @@
 	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
 		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
 	      res_inst_tac [("act", sact)] transient_mem 2,
+                 (*simplify the command's domain*)
 	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
-	      simp_tac (simpset() addsimps [main_def]) 2,
+	         (*INSIST that the command belongs to the program*)
+	      force_tac (claset(), simpset() addsimps [main_def]) 2,
 	      constrains_tac (main_def::cmd_defs) 1,
 	      rewrite_goals_tac cmd_defs,
 	      ALLGOALS Clarify_tac,
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -14,6 +14,14 @@
 
 (*** constrains ***)
 
+(*Map the type (anything => ('a set => anything) to just 'a*)
+fun overload_2nd_set s =
+    Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
+
+overload_2nd_set "UNITY.constrains";
+overload_2nd_set "UNITY.stable";
+overload_2nd_set "UNITY.unless";
+
 val prems = Goalw [constrains_def]
     "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
 \    ==> constrains acts A A'";
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Wed Aug 19 10:34:31 1998 +0200
@@ -9,6 +9,14 @@
 *)
 
 
+(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*)
+Blast.overloaded ("WFair.leadsto", 
+		  #1 o HOLogic.dest_prodT o 
+		  HOLogic.dest_setT o HOLogic.dest_setT o domain_type);
+
+overload_2nd_set "WFair.transient";
+overload_2nd_set "WFair.ensures";
+
 (*** transient ***)
 
 Goalw [stable_def, constrains_def, transient_def]
@@ -52,8 +60,7 @@
 
 Goalw [ensures_def, constrains_def, transient_def]
     "acts ~= {} ==> ensures acts A UNIV";
-by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
-by (Blast_tac 1);
+by Auto_tac;
 qed "ensures_UNIV";
 
 Goalw [ensures_def]
@@ -165,9 +172,9 @@
 
 Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
 \   ==> leadsTo acts B B'";
-(*PROOF FAILED: why?*)
-by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
-			       leadsTo_weaken_L]) 1);
+(*PROOF FAILED unless leadsTo_Trans is last*)
+by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
+			       leadsTo_Trans]) 1);
 qed "leadsTo_weaken";
 
 
@@ -468,7 +475,7 @@
 (*** Completion: Binary and General Finite versions ***)
 
 Goal "[| leadsTo acts A A';  stable acts A';   \
-\      leadsTo acts B B';  stable acts B';  id: acts |] \
+\        leadsTo acts B B';  stable acts B';  id: acts |] \
 \   ==> leadsTo acts (A Int B) (A' Int B')";
 by (subgoal_tac "stable acts (wlt acts B')" 1);
 by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
@@ -483,8 +490,8 @@
 by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
 by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
 			       subset_imp_leadsTo]) 2);
-(*Blast_tac gives PROOF FAILED*)
-by (best_tac (claset() addIs [leadsTo_Trans]) 1);
+(*addIs looks safer, but loops with PROOF FAILED*)
+by (blast_tac (claset() addSIs [leadsTo_Trans]) 1);
 qed "stable_completion";
 
 
diff -r 22c195854229 -r d75c03cf77b5 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Aug 19 10:29:01 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy	Wed Aug 19 10:34:31 1998 +0200
@@ -21,11 +21,12 @@
     "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
 			(*(unless acts A B) would be equivalent*)
 
-consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
-       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
   
 translations
   "leadsTo acts A B" == "(A,B) : leadsto acts"
+  "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
 
 inductive "leadsto acts"
   intrs