# HG changeset patch
# User paulson
# Date 903024400 -7200
# Node ID 1861a564d7e2041e33475fbf5b6cbe0b4aaa80b5
# Parent  b380921982b9595d5b6eb5de16969794b055fb5b
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them

diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -11,25 +11,21 @@
 *)
 
 (*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
-\     ==> stable acts (atMost n)";
-by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
+Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
+\     ==> Stable prg (atMost n)";
+by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
-			 constrains_def, le_max_iff_disj]) 1);
-by (Clarify_tac 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (blast_tac (claset() addSEs [subsetCE]
-			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
+    (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
+			 le_max_iff_disj]) 1);
+by (etac Constrains_weaken_R 1);
+by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
 qed "common_stable";
 
-Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
-\     ==> invariant (|Init={0}, Acts=acts|) (atMost n)";
-by (rtac invariantI 1);
-by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
-by (simp_tac (simpset() addsimps [atMost_def]) 1);
-qed "common_invariant";
+Goal "[| Init prg <= atMost n;  \
+\        ALL m. Constrains prg {m} (maxfg m); n: common |] \
+\     ==> Invariant prg (atMost n)";
+by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
+qed "common_Invariant";
 
 
 (*** Some programs that implement the safety property above ***)
@@ -71,23 +67,23 @@
 
 Addsimps [atMost_Int_atLeast];
 
-Goal "[| ALL m. constrains acts {m} (maxfg m); \
-\               ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
-\               n: common;  id: acts |]  \
-\            ==> leadsTo acts (atMost n) common";
-by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
+Goal "[| ALL m. Constrains prg {m} (maxfg m); \
+\               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
+\               n: common;  id: Acts prg |]  \
+\            ==> LeadsTo prg (atMost n) common";
+by (rtac LeadsTo_weaken_R 1);
+by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac subset_refl 2);
-by (blast_tac (claset() addDs [psp_stable2] 
-                        addIs [common_stable, leadsTo_weaken_R]) 1);
+by (blast_tac (claset() addDs [PSP_stable2] 
+                        addIs [common_stable, LeadsTo_weaken_R]) 1);
 val lemma = result();
 
 (*The "ALL m: Compl common" form echoes CMT6.*)
-Goal "[| ALL m. constrains acts {m} (maxfg m); \
-\               ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
-\               n: common;  id: acts |]  \
-\            ==> leadsTo acts (atMost (LEAST n. n: common)) common";
+Goal "[| ALL m. Constrains prg {m} (maxfg m); \
+\               ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
+\               n: common;  id: Acts prg |]  \
+\            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
 by (rtac lemma 1);
 by (ALLGOALS Asm_simp_tac);
 by (etac LeastI 2);
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Common.thy
--- a/src/HOL/UNITY/Common.thy	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Common.thy	Thu Aug 13 18:06:40 1998 +0200
@@ -10,7 +10,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
 *)
 
-Common = WFair + Traces +
+Common = SubstAx +
 
 consts
   ftime,gtime :: nat=>nat
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Constrains.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Constrains.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -0,0 +1,262 @@
+(*  Title:      HOL/UNITY/Constrains
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+*)
+
+
+
+(**MOVE TO EQUALITIES.ML**)
+
+Goal "(A Un B <= C) = (A <= C & B <= C)";
+by (Blast_tac 1);
+qed "Un_subset_iff";
+
+Goal "(C <= A Int B) = (C <= A & C <= B)";
+by (Blast_tac 1);
+qed "Int_subset_iff";
+
+
+(*** Constrains ***)
+
+(*constrains (Acts prg) B B'
+  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
+bind_thm ("constrains_reachable_Int",
+	  subset_refl RS
+	  rewrite_rule [stable_def] stable_reachable RS 
+	  constrains_Int);
+
+Goalw [Constrains_def]
+    "constrains (Acts prg) A A' ==> Constrains prg A A'";
+by (etac constrains_reachable_Int 1);
+qed "constrains_imp_Constrains";
+
+val prems = Goal
+    "(!!act s s'. [| act: Acts prg;  (s,s') : act;  s: A |] ==> s': A') \
+\    ==> Constrains prg A A'";
+by (rtac constrains_imp_Constrains 1);
+by (blast_tac (claset() addIs (constrainsI::prems)) 1);
+qed "ConstrainsI";
+
+Goalw [Constrains_def, constrains_def] "Constrains prg {} B";
+by (Blast_tac 1);
+qed "Constrains_empty";
+
+Goal "Constrains prg A UNIV";
+by (blast_tac (claset() addIs [ConstrainsI]) 1);
+qed "Constrains_UNIV";
+AddIffs [Constrains_empty, Constrains_UNIV];
+
+
+Goalw [Constrains_def]
+    "[| Constrains prg A A'; A'<=B' |] ==> Constrains prg A B'";
+by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
+qed "Constrains_weaken_R";
+
+Goalw [Constrains_def]
+    "[| Constrains prg A A'; B<=A |] ==> Constrains prg B A'";
+by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
+qed "Constrains_weaken_L";
+
+Goalw [Constrains_def]
+   "[| Constrains prg A A'; B<=A; A'<=B' |] ==> Constrains prg B B'";
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "Constrains_weaken";
+
+(** Union **)
+
+Goalw [Constrains_def]
+    "[| Constrains prg A A'; Constrains prg B B' |]   \
+\    ==> Constrains prg (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
+qed "Constrains_Un";
+
+Goalw [Constrains_def]
+    "ALL i:I. Constrains prg (A i) (A' i) \
+\    ==> Constrains prg (UN i:I. A i) (UN i:I. A' i)";
+by (dtac ball_constrains_UN 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "ball_Constrains_UN";
+
+(** Intersection **)
+
+Goalw [Constrains_def]
+    "[| Constrains prg A A'; Constrains prg B B' |]   \
+\    ==> Constrains prg (A Int B) (A' Int B')";
+by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
+qed "Constrains_Int";
+
+Goalw [Constrains_def]
+    "[| 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);
+qed "ball_Constrains_INT";
+
+Goalw [Constrains_def]
+     "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
+by (dtac constrains_imp_subset 1);
+by (assume_tac 1);
+by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
+qed "Constrains_imp_subset";
+
+Goalw [Constrains_def]
+    "[| id: Acts prg; Constrains prg A B; Constrains prg B C |]   \
+\    ==> Constrains prg A C";
+by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
+qed "Constrains_trans";
+
+
+(*** Stable ***)
+
+Goal "Stable prg A = stable (Acts prg) (reachable prg Int A)";
+by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
+qed "Stable_eq_stable";
+
+Goalw [Stable_def] "Constrains prg A A ==> Stable prg A";
+by (assume_tac 1);
+qed "StableI";
+
+Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
+by (assume_tac 1);
+qed "StableD";
+
+Goalw [Stable_def]
+    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
+by (blast_tac (claset() addIs [Constrains_Un]) 1);
+qed "Stable_Un";
+
+Goalw [Stable_def]
+    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Int A')";
+by (blast_tac (claset() addIs [Constrains_Int]) 1);
+qed "Stable_Int";
+
+Goalw [Stable_def]
+    "[| Stable prg C; Constrains prg A (C Un A') |]   \
+\    ==> Constrains prg (C Un A) (C Un A')";
+by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Un";
+
+Goalw [Stable_def]
+    "[| Stable prg C; Constrains prg (C Int A) A' |]   \
+\    ==> Constrains prg (C Int A) (C Int A')";
+by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Int";
+
+Goalw [Stable_def]
+    "(ALL i:I. Stable prg (A i)) ==> Stable prg (INT i:I. A i)";
+by (etac ball_Constrains_INT 1);
+qed "ball_Stable_INT";
+
+Goal "Stable prg (reachable prg)";
+by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
+qed "Stable_reachable";
+
+
+
+(*** The Elimination Theorem.  The "free" m has become universally quantified!
+     Should the premise be !!m instead of ALL m ?  Would make it harder to use
+     in forward proof. ***)
+
+Goalw [Constrains_def, constrains_def]
+    "[| ALL m. Constrains prg {s. s x = m} (B m) |] \
+\    ==> Constrains prg {s. s x : M} (UN m:M. B m)";
+by (Blast_tac 1);
+qed "Elimination";
+
+(*As above, but for the trivial case of a one-variable state, in which the
+  state is identified with its one variable.*)
+Goalw [Constrains_def, constrains_def]
+    "(ALL m. Constrains prg {m} (B m)) ==> Constrains prg M (UN m:M. B m)";
+by (Blast_tac 1);
+qed "Elimination_sing";
+
+Goalw [Constrains_def, constrains_def]
+   "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
+\   ==> Constrains prg A (A' Un B')";
+by (Blast_tac 1);
+qed "Constrains_cancel";
+
+
+(*** Specialized laws for handling Invariants ***)
+
+(** Natural deduction rules for "Invariant prg A" **)
+
+Goal "[| Init prg<=A;  Stable prg A |] ==> Invariant prg A";
+by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
+qed "InvariantI";
+
+Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
+by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
+qed "InvariantD";
+
+bind_thm ("InvariantE", InvariantD RS conjE);
+
+
+(*The set of all reachable states is an Invariant...*)
+Goal "Invariant prg (reachable prg)";
+by (simp_tac (simpset() addsimps [Invariant_def]) 1);
+by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
+qed "Invariant_reachable";
+
+(*...in fact the strongest Invariant!*)
+Goal "Invariant prg A ==> reachable prg <= A";
+by (full_simp_tac 
+    (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
+			 Invariant_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "Invariant_includes_reachable";
+
+
+Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
+by (dtac Invariant_includes_reachable 1);
+by (Blast_tac 1);
+qed "reachable_Int_INV";
+
+Goal "[| Invariant prg INV;  Constrains prg (INV Int A) A' |]   \
+\     ==> Constrains prg A A'";
+by (asm_full_simp_tac
+    (simpset() addsimps [Constrains_def, reachable_Int_INV,
+			 Int_assoc RS sym]) 1);
+qed "Invariant_ConstrainsI";
+
+bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
+
+Goal "[| Invariant prg INV;  Constrains prg A A' |]   \
+\     ==> Constrains prg A (INV Int A')";
+by (asm_full_simp_tac
+    (simpset() addsimps [Constrains_def, reachable_Int_INV,
+			 Int_assoc RS sym]) 1);
+qed "Invariant_ConstrainsD";
+
+bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
+
+
+
+(** Conjoining Invariants **)
+
+Goal "[| Invariant prg A;  Invariant prg B |] ==> Invariant prg (A Int B)";
+by (auto_tac (claset(),
+	      simpset() addsimps [Invariant_def, Stable_Int]));
+qed "Invariant_Int";
+
+(*Delete the nearest invariance assumption (which will be the second one
+  used by Invariant_Int) *)
+val Invariant_thin =
+    read_instantiate_sg (sign_of thy)
+                [("V", "Invariant ?Prg ?A")] thin_rl;
+
+(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
+val Invariant_Int_tac = dtac Invariant_Int THEN' 
+                        assume_tac THEN'
+			etac Invariant_thin;
+
+(*Combines two invariance THEOREMS into one.*)
+val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
+
+
+
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Constrains.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Constrains.thy	Thu Aug 13 18:06:40 1998 +0200
@@ -0,0 +1,28 @@
+(*  Title:      HOL/UNITY/Constrains
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+*)
+
+Constrains = UNITY + Traces + 
+
+constdefs
+
+  Constrains :: "['a program, 'a set, 'a set] => bool"
+    "Constrains prg A B == 
+		 constrains (Acts prg)
+                            (reachable prg  Int  A)
+  		            (reachable prg  Int  B)"
+
+  Stable     :: "'a program => 'a set => bool"
+    "Stable prg A == Constrains prg A A"
+
+  Unless :: "['a program, 'a set, 'a set] => bool"
+    "Unless prg A B == Constrains prg (A-B) (A Un B)"
+
+  Invariant :: "['a program, 'a set] => bool"
+  "Invariant prg A == (Init prg) <= A & Stable prg A"
+
+end
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -22,40 +22,40 @@
 AddIffs [id_in_Acts];
 
 
-Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
-by (rtac invariantI 1);
-by (force_tac (claset(), 
-	       simpset() addsimps [Join_def]) 1);
-by (auto_tac (claset(), simpset() addsimps [stable_Join]));
+Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
+by (rtac InvariantI 1);
+by (Force_tac 1);
+by (rtac (constrains_imp_Constrains RS StableI) 1);
+by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
 by (constrains_tac [prgG_def,cmdG_def] 2);
 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
 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}";
-br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+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}";
-br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+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);
 qed "lemma2_2";
 
 
 Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
-br LeadsTo_weaken_R 1;
+by (rtac LeadsTo_weaken_R 1);
 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}*)
-br LeadsTo_Diff 1;
-br lemma2_2 2;
-br LeadsTo_Trans 1;
-br lemma2_2 2;
-br (lemma2_1 RS LeadsTo_weaken_L) 1;
+by (rtac LeadsTo_Diff 1);
+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 Auto_tac;
 qed "progress";
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -44,34 +44,36 @@
 qed "less_imp_le_pred";
 
 
-Goalw [Lprg_def] "invariant Lprg open_stop";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg open_stop";
+by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 qed "open_stop";
 
-Goalw [Lprg_def] "invariant Lprg stop_floor";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg stop_floor";
+by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 qed "stop_floor";
 
-(*Should not have to prove open_stop concurrently!!*)
-Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
-by (rtac invariantI 1);
+(*This one needs open_stop, which was proved above*)
+Goal "Invariant Lprg open_move";
+by (rtac InvariantI 1);
+br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
+bw Lprg_def;
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 qed "open_move";
 
-Goalw [Lprg_def] "invariant Lprg moving_up";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg moving_up";
+by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
 qed "moving_up";
 
-Goalw [Lprg_def] "invariant Lprg moving_down";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg moving_down";
+by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
@@ -82,8 +84,8 @@
 
 xxxxxxxxxxxxxxxx;
 
-Goalw [Lprg_def] "invariant Lprg bounded";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg bounded";
+by (rtac InvariantI 1);
 by (Force_tac 1);
 by (constrains_tac (cmd_defs@always_defs) 1);
 by (ALLGOALS
@@ -94,8 +96,8 @@
 by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
 qed "bounded";
 
-Goalw [Lprg_def] "invariant Lprg invariantV";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg invariantV";
+by (rtac InvariantI 1);
 by (constrains_tac cmd_defs 2);
 by Auto_tac;
 qed "invariantV";
@@ -122,7 +124,7 @@
 
 Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
 by (cut_facts_tac [invariantUV] 1);
-bw Lprg_def;
+by (rewtac Lprg_def);
 by (ensures_tac cmd_defs "cmd2U" 1);
 qed "U_F2";
 
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -26,34 +26,35 @@
 
 Addsimps update_defs;
 
-
 Addsimps [invariantU_def, invariantV_def];
 
 
-Goalw [Mprg_def] "invariant Mprg invariantU";
-by (rtac invariantI 1);
+Goalw [Mprg_def] "Invariant Mprg invariantU";
+by (rtac InvariantI 1);
 by (constrains_tac cmd_defs 2);
 by Auto_tac;
 qed "invariantU";
 
-Goalw [Mprg_def] "invariant Mprg invariantV";
-by (rtac invariantI 1);
+Goalw [Mprg_def] "Invariant Mprg invariantV";
+by (rtac InvariantI 1);
 by (constrains_tac cmd_defs 2);
 by Auto_tac;
 qed "invariantV";
 
-val invariantUV = invariant_Int_rule [invariantU, invariantV];
+val invariantUV = Invariant_Int_rule [invariantU, invariantV];
 
 
 (*The safety property: mutual exclusion*)
 Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
-by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
+by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
 by Auto_tac;
 qed "mutual_exclusion";
 
 
 (*The bad invariant FAILS in cmd1V*)
-Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU";
+Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
+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]));
@@ -67,7 +68,7 @@
 
 (*** Progress for U ***)
 
-Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}";
+Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
 by (constrains_tac cmd_defs 1);
 qed "U_F0";
 
@@ -77,13 +78,12 @@
 
 Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
 by (cut_facts_tac [invariantUV] 1);
-bw Mprg_def;
+by (rewtac Mprg_def);
 by (ensures_tac cmd_defs "cmd2U" 1);
 qed "U_F2";
 
 Goal "LeadsTo Mprg {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 (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);
 qed "U_F3";
@@ -109,15 +109,15 @@
 
 (*Misra's F4*)
 Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
-by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
+by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
 by Auto_tac;
-qed "u_leadsto_p";
+qed "u_Leadsto_p";
 
 
 (*** Progress for V ***)
 
 
-Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}";
+Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
 by (constrains_tac cmd_defs 1);
 qed "V_F0";
 
@@ -131,8 +131,7 @@
 qed "V_F2";
 
 Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
-by (rtac leadsTo_imp_LeadsTo 1); 
-by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
+by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
 by (ensures_tac cmd_defs "cmd4V" 2);
 by (ensures_tac cmd_defs "cmd3V" 1);
 qed "V_F3";
@@ -159,9 +158,9 @@
 
 (*Misra's F4*)
 Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
-by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
+by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
 by Auto_tac;
-qed "v_leadsto_not_p";
+qed "v_Leadsto_not_p";
 
 
 (** Absence of starvation **)
@@ -174,10 +173,10 @@
 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 ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "m1_leadsto_3";
+qed "m1_Leadsto_3";
 
 
 (*The same for V*)
@@ -188,7 +187,7 @@
 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 ([u_Leadsto_p, V_F0] MRS PSP_Unless  RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "n1_leadsto_3";
+qed "n1_Leadsto_3";
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -31,8 +31,8 @@
 
 Addsimps [reach_invariant_def];
 
-Goalw [Rprg_def] "invariant Rprg reach_invariant";
-by (rtac invariantI 1);
+Goalw [Rprg_def] "Invariant Rprg reach_invariant";
+by (rtac InvariantI 1);
 by Auto_tac;  (*for the initial state; proof of stability remains*)
 by (constrains_tac [Rprg_def, asgt_def] 1);
 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
@@ -117,38 +117,31 @@
 	      simpset() addsimps [fun_upd_idem]));
 qed "metric_le";
 
-Goal "(u,v): edges ==> \
-\              ensures (Acts Rprg) ((metric-``{m}) Int {s. s u & ~ s v})  \
-\                            (metric-``(lessThan m))";
-by (ensures_tac [Rprg_def, asgt_def] "asgt u v" 1);
-by (cut_facts_tac [metric_le] 1);
-by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
-qed "edges_ensures";
-
-Goal "leadsTo (Acts Rprg) ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
 by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
-by (rtac leadsTo_UN 1);
-by (split_all_tac 1);
-by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
-qed "leadsTo_Diff_fixedpoint";
+by (rtac LeadsTo_UN 1);
+by Auto_tac;
+by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
+by (cut_facts_tac [metric_le RS le_imp_less_or_eq] 1);
+by (Fast_tac 1);
+qed "LeadsTo_Diff_fixedpoint";
 
-Goal "leadsTo (Acts Rprg) (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
-by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
-qed "leadsTo_Un_fixedpoint";
+Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+qed "LeadsTo_Un_fixedpoint";
 
 
 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
-Goal "leadsTo (Acts Rprg) UNIV fixedpoint";
-by (rtac lessThan_induct 1);
+Goal "LeadsTo Rprg UNIV fixedpoint";
+by (rtac LessThan_induct 1);
 by Auto_tac;
-by (rtac leadsTo_Un_fixedpoint 1);
-qed "leadsTo_fixedpoint";
+by (rtac LeadsTo_Un_fixedpoint 1);
+qed "LeadsTo_fixedpoint";
 
 Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
 by (stac (fixedpoint_invariant_correct RS sym) 1);
-by (rtac ([reach_invariant,
-	   leadsTo_fixedpoint RS leadsTo_imp_LeadsTo] 
-	  MRS invariant_LeadsTo_weaken) 1); 
+by (rtac ([reach_invariant, LeadsTo_fixedpoint] 
+	  MRS Invariant_LeadsTo_weaken) 1); 
 by Auto_tac;
 qed "LeadsTo_correct";
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -7,32 +7,22 @@
 *)
 
 
-(*constrains (Acts prg) B B'
-  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
-bind_thm ("constrains_reachable",
-	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
-
 
 (*** Specialized laws for handling invariants ***)
 
-Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
-bd invariant_includes_reachable 1;
-by (Blast_tac 1);
-qed "reachable_Int_INV";
-
-Goal "[| invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
+Goal "[| Invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
 \     ==> LeadsTo prg A A'";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
 			 Int_assoc RS sym]) 1);
-qed "invariant_LeadsToI";
+qed "Invariant_LeadsToI";
 
-Goal "[| invariant prg INV;  LeadsTo prg A A' |]   \
+Goal "[| Invariant prg INV;  LeadsTo prg A A' |]   \
 \     ==> LeadsTo prg A (INV Int A')";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
 			 Int_assoc RS sym]) 1);
-qed "invariant_LeadsToD";
+qed "Invariant_LeadsToD";
 
 
 (*** Introduction rules: Basis, Trans, Union ***)
@@ -42,9 +32,6 @@
 by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
 qed "leadsTo_imp_LeadsTo";
 
-(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
-bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
-
 Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] ==> LeadsTo prg A C";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
@@ -138,33 +125,37 @@
 qed "LeadsTo_weaken";
 
 
-(** More rules using the premise "invariant prg" **)
+(** More rules using the premise "Invariant prg" **)
 
-Goal "[| invariant prg INV;      \
-\        constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
+Goalw [LeadsTo_def, Constrains_def]
+     "[| Constrains prg (A-A') (A Un A'); transient  (Acts prg) (A-A') |]   \
+\     ==> LeadsTo prg A A'";
+by (rtac (ensuresI RS leadsTo_Basis) 1);
+by (blast_tac (claset() addIs [transient_strengthen]) 2);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "LeadsTo_Basis";
+
+Goal "[| Invariant prg INV;      \
+\        Constrains prg (INV Int (A-A')) (A Un A'); \
 \        transient  (Acts prg) (INV Int (A-A')) |]   \
 \ ==> LeadsTo prg A A'";
-br invariant_LeadsToI 1;
-ba 1;
-by (rtac (ensuresI RS LeadsTo_Basis) 1);
-by (ALLGOALS 
-    (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym, 
-					Diff_Int_distrib RS sym])));
-be invariantE 1;
-by (blast_tac (claset() addSDs [stable_constrains_Int]
-			addIs [constrains_weaken]) 1);
-qed "invariant_LeadsTo_Basis";
+by (rtac Invariant_LeadsToI 1);
+by (assume_tac 1);
+by (rtac LeadsTo_Basis 1);
+by (blast_tac (claset() addIs [transient_strengthen]) 2);
+by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
+qed "Invariant_LeadsTo_Basis";
 
-Goal "[| invariant prg INV;      \
+Goal "[| Invariant prg INV;      \
 \        LeadsTo prg A A'; id: Acts prg;   \
 \        INV Int B  <= A;  INV Int A' <= B' |] \
 \     ==> LeadsTo prg B B'";
-br invariant_LeadsToI 1;
-ba 1;
-bd invariant_LeadsToD 1;
-ba 1;
+by (rtac Invariant_LeadsToI 1);
+by (assume_tac 1);
+by (dtac Invariant_LeadsToD 1);
+by (assume_tac 1);
 by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
-qed "invariant_LeadsTo_weaken";
+qed "Invariant_LeadsTo_weaken";
 
 
 (*Set difference: maybe combine with leadsTo_weaken_L??
@@ -250,43 +241,39 @@
 (** PSP: Progress-Safety-Progress **)
 
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
-Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
-\     ==> LeadsTo prg (A Int B) (A' Int B)";
-by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, 
-					   psp_stable]) 1);
+Goal
+  "[| LeadsTo prg A A';  Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (dtac psp_stable 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
 qed "PSP_stable";
 
-Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
+Goal "[| LeadsTo prg A A'; Stable prg B |] \
 \     ==> LeadsTo prg (B Int A) (B Int A')";
 by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
 qed "PSP_stable2";
 
-
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
+Goalw [LeadsTo_def, Constrains_def]
+     "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (dtac psp 1);
-by (etac constrains_reachable 1);
-by (etac leadsTo_weaken 2);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
 qed "PSP";
 
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
 \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
 qed "PSP2";
 
-Goalw [unless_def]
-   "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
+Goalw [Unless_def]
+     "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
 by (dtac PSP 1);
 by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
-by (etac LeadsTo_Diff 2);
-by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
-by Auto_tac;
-qed "PSP_unless";
+by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
+			       subset_imp_LeadsTo]) 2);
+by (assume_tac 1);
+qed "PSP_Unless";
 
 
 (*** Induction rules ***)
@@ -294,7 +281,7 @@
 (** Meta or object quantifier ????? **)
 Goal "[| wf r;     \
 \        ALL m. LeadsTo prg (A Int f-``{m})                     \
-\                                 ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\                           ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \        id: Acts prg |] \
 \     ==> LeadsTo prg A B";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
@@ -353,49 +340,42 @@
 
 (*** Completion: Binary and General Finite versions ***)
 
-Goal "[| LeadsTo prg A A';  stable (Acts prg) A';   \
-\        LeadsTo prg B B';  stable (Acts prg) B';  id: Acts prg |] \
+Goal "[| LeadsTo prg A A';  Stable prg A';   \
+\        LeadsTo prg B B';  Stable prg B';  id: Acts prg |] \
 \     ==> LeadsTo prg (A Int B) (A' Int B')";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
-                        addSIs [stable_Int, stable_reachable]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
 qed "Stable_completion";
 
 
-Goal "[| finite I;  id: Acts prg |]                     \
+Goal "[| finite I;  id: Acts prg |]      \
 \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
-\         (ALL i:I. stable (Acts prg) (A' i)) -->         \
+\         (ALL i:I. Stable prg (A' i)) -->         \
 \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
 by (etac finite_induct 1);
 by (Asm_simp_tac 1);
-by (asm_simp_tac 
-    (simpset() addsimps [Stable_completion, stable_def, 
-			 ball_constrains_INT]) 1);
+by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
 qed_spec_mp "Finite_stable_completion";
 
 
-Goal "[| LeadsTo prg A (A' Un C);  constrains (Acts prg) A' (A' Un C); \
-\        LeadsTo prg B (B' Un C);  constrains (Acts prg) B' (B' Un C); \
+Goal "[| LeadsTo prg A (A' Un C);  Constrains prg A' (A' Un C); \
+\        LeadsTo prg B (B' Un C);  Constrains prg B' (B' Un C); \
 \        id: Acts prg |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
-by (dtac completion 1);
-by (assume_tac 2);
-by (ALLGOALS 
-    (asm_simp_tac 
-     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
-by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
+				       Int_Un_distrib]) 1);
+by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
 qed "Completion";
 
 
 Goal "[| finite I;  id: Acts prg |] \
 \     ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) -->  \
-\         (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
+\         (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
 \         LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
-by (dtac ball_constrains_INT 1);
+by (dtac ball_Constrains_INT 1);
 by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
 qed "Finite_completion";
 
@@ -408,22 +388,22 @@
 (*proves "constrains" properties when the program is specified*)
 fun constrains_tac (main_def::cmd_defs) = 
    SELECT_GOAL
-      (EVERY [TRY (rtac stableI 1),
+      (EVERY [REPEAT (resolve_tac [StableI, stableI,
+				   constrains_imp_Constrains] 1),
 	      rtac constrainsI 1,
 	      full_simp_tac (simpset() addsimps [main_def]) 1,
-	      REPEAT_FIRST (eresolve_tac [disjE]),
+	      REPEAT_FIRST (etac disjE ),
 	      rewrite_goals_tac cmd_defs,
 	      ALLGOALS (SELECT_GOAL Auto_tac)]);
 
 
-(*proves "ensures" properties when the program is specified*)
+(*proves "ensures/leadsTo" properties when the program is specified*)
 fun ensures_tac (main_def::cmd_defs) sact = 
     SELECT_GOAL
-      (EVERY [REPEAT (invariant_Int_tac 1),
-	      etac invariant_LeadsTo_Basis 1 
+      (EVERY [REPEAT (Invariant_Int_tac 1),
+	      etac Invariant_LeadsTo_Basis 1 
 	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
-		  REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, 
-				    ensuresI] 1),
+		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
 	      res_inst_tac [("act", sact)] transient_mem 2,
 	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
 	      simp_tac (simpset() addsimps [main_def]) 2,
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 13 18:06:40 1998 +0200
@@ -6,7 +6,7 @@
 LeadsTo relation: restricted to the set of reachable states.
 *)
 
-SubstAx = WFair + Traces + 
+SubstAx = WFair + Constrains + 
 
 constdefs
 
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -16,59 +16,7 @@
 by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
 qed "reachable_equiv_traces";
 
-Goal "stable (Acts prg) (reachable prg)";
+Goal "acts <= Acts prg ==> stable acts (reachable prg)";
 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
 qed "stable_reachable";
 
-(*The set of all reachable states is an invariant...*)
-Goal "invariant prg (reachable prg)";
-by (simp_tac (simpset() addsimps [invariant_def]) 1);
-by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
-qed "invariant_reachable";
-
-(*...in fact the strongest invariant!*)
-Goal "invariant prg A ==> reachable prg <= A";
-by (full_simp_tac 
-    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
-by (rtac subsetI 1);
-by (etac reachable.induct 1);
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "invariant_includes_reachable";
-
-
-(** Natural deduction rules for "invariant prg A" **)
-
-Goal "[| (Init prg)<=A;  stable (Acts prg) A |] ==> invariant prg A";
-by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantI";
-
-Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantD";
-
-bind_thm ("invariantE", invariantD RS conjE);
-
-
-(** Conjoining invariants **)
-
-Goal "[| invariant prg A;  invariant prg B |] \
-\     ==> invariant prg (A Int B)";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1);
-by Auto_tac;
-qed "invariant_Int";
-
-(*Delete the nearest invariance assumption (which will be the second one
-  used by invariant_Int) *)
-val invariant_thin =
-    read_instantiate_sg (sign_of thy)
-                [("V", "invariant ?Prg ?A")] thin_rl;
-
-(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
-val invariant_Int_tac = dtac invariant_Int THEN' 
-                        assume_tac THEN'
-			etac invariant_thin;
-
-(*Combines two invariance THEOREMS into one.*)
-val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int);
-
-
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy	Thu Aug 13 18:06:40 1998 +0200
@@ -38,8 +38,4 @@
     Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
 	   ==> s' : reachable prg"
 
-constdefs
-  invariant :: "['a program, 'a set] => bool"
-  "invariant prg A == (Init prg) <= A & stable (Acts prg) A"
-
 end
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -21,8 +21,7 @@
 qed "constrainsI";
 
 Goalw [constrains_def]
-    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] \
-\            ==> s': A'";
+    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] ==> s': A'";
 by (Blast_tac 1);
 qed "constrainsD";
 
@@ -90,8 +89,7 @@
 by (Blast_tac 1);
 qed "all_constrains_INT";
 
-Goalw [constrains_def]
-    "[| constrains acts A A'; id: acts |] ==> A<=A'";
+Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
 by (Blast_tac 1);
 qed "constrains_imp_subset";
 
@@ -104,25 +102,21 @@
 
 (*** stable ***)
 
-Goalw [stable_def]
-    "constrains acts A A ==> stable acts A";
+Goalw [stable_def] "constrains acts A A ==> stable acts A";
 by (assume_tac 1);
 qed "stableI";
 
-Goalw [stable_def]
-    "stable acts A ==> constrains acts A A";
+Goalw [stable_def] "stable acts A ==> constrains acts A A";
 by (assume_tac 1);
 qed "stableD";
 
 Goalw [stable_def]
-    "[| stable acts A; stable acts A' |]   \
-\    ==> stable acts (A Un A')";
+    "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
 by (blast_tac (claset() addIs [constrains_Un]) 1);
 qed "stable_Un";
 
 Goalw [stable_def]
-    "[| stable acts A; stable acts A' |]   \
-\    ==> stable acts (A Int A')";
+    "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
 by (blast_tac (claset() addIs [constrains_Int]) 1);
 qed "stable_Int";
 
@@ -144,15 +138,15 @@
   in forward proof.*)
 Goalw [constrains_def]
     "[| ALL m. constrains acts {s. s x = m} (B m) |] \
-\    ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
+\    ==> constrains acts {s. s x : M} (UN m:M. B m)";
 by (Blast_tac 1);
 qed "elimination";
 
+
 (*As above, but for the trivial case of a one-variable state, in which the
   state is identified with its one variable.*)
 Goalw [constrains_def]
-    "[| ALL m. constrains acts {m} (B m) |] \
-\    ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
+    "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
 by (Blast_tac 1);
 qed "elimination_sing";
 
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Thu Aug 13 18:06:40 1998 +0200
@@ -11,133 +11,35 @@
     Maybe Join instead of Un, and JOIN for UNION
 *)
 
-(*** Safety: constrains, stable, FP ***)
-
-Goalw [constrains_def]
-    "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
-by (Blast_tac 1);
-qed "constrains_UN";
-
-Goalw [constrains_def]
-    "constrains (actsF Un actsG) A B =  \
-\    (constrains actsF A B & constrains actsG A B)";
-by (simp_tac (simpset() addsimps [ball_Un]) 1);
-qed "constrains_Un";
-
-(*Provable by constrains_Un and constrains_weaken, but why bother?*)
-Goalw [constrains_def]
-     "[| constrains actsF A A';  constrains actsG B B' |] \
-\     ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
-by (Blast_tac 1);
-qed "constrains_Un_weaken";
 
-Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
-by (simp_tac (simpset() addsimps [constrains_UN]) 1);
-qed "stable_UN";
-
-Goalw [stable_def]
-    "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
-by (simp_tac (simpset() addsimps [constrains_Un]) 1);
-qed "stable_Un";
+Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Init_Join";
 
-Goal "stable (Acts (Join prgF prgG)) A = \
-\     (stable (Acts prgF) A & stable (Acts prgG) A)";
-by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
-qed "stable_Join";
-
-Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
-by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
-qed "FP_UN";
-
-
-(*** Progress: transient, ensures ***)
-
-Goalw [transient_def]
-    "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
-by (Simp_tac 1);
-qed "transient_UN";
+Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Acts_Join";
 
-Goalw [ensures_def,transient_def]
-    "ensures (UN i:I. acts i) A B = \
-\    ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
-\     (EX i:I. ensures (acts i) A B))";
-by (simp_tac (simpset() addsimps [constrains_UN]) 1);
-by Auto_tac;
-qed "ensures_UN";
-
-(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
-Goal "ensures (actsF Un actsG) A B =     \
-\     (constrains actsF (A-B) (A Un B) & \
-\      constrains actsG (A-B) (A Un B) & \
-\      (ensures actsF A B | ensures actsG A B))";
-by (simp_tac (simpset() addcongs [conj_cong]
-			addsimps [ensures_UN, Un_eq_UN,
-				  all_bool_eq, ex_bool_eq]) 1);
-qed "ensures_Un";
-
-(*Or a longer proof via constrains_imp_subset*)
-Goalw [stable_def, constrains_def]
-     "[| stable actsF A;  constrains actsG A A';  id: actsG |] \
-\     ==> constrains (actsF Un actsG) A A'";
-by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
-by (Blast_tac 1);
-qed "stable_constrains_Un";
+Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+qed "Init_JN";
 
-Goalw [Join_def]
-      "[| stable (Acts prgF) A;  invariant prgG A |]     \
-\      ==> invariant (Join prgF prgG) A";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
-by (Blast_tac 1);
-qed "stable_Join_invariant";
-
-Goal "[| stable actsF A;  ensures actsG A B |]     \
-\     ==> ensures (actsF Un actsG) A B";
-by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
-by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
-by (etac constrains_weaken 1);
-by Auto_tac;
-qed "ensures_stable_Un1";
+Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+qed "Acts_JN";
 
-Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
-\     ==> ensures (Acts (Join prgF prgG)) A B";
-by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
-qed "ensures_stable_Join1";
-
-(*As above, but exchanging the roles of F and G*)
-Goal "[| ensures actsF A B;  stable actsG A |]     \
-\     ==> ensures (actsF Un actsG) A B";
-by (stac Un_commute 1);
-by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
-qed "ensures_stable_Un2";
-
-Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
-\     ==> ensures (Acts (Join prgF prgG)) A B";
-by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
-qed "ensures_stable_Join2";
-
+Addsimps [Init_Join, Init_JN];
 
 (** Theoretical issues **)
 
-Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
-by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
+Goal "Join prgF prgG = Join prgG prgF";
+by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
 qed "Join_commute";
 
-Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
-by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
+Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
+by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
 qed "Join_assoc";
 
-(**NOT PROVABLE because no "surjective pairing" for records
-Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
-by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
-qed "Join_Null";
-*)
-
-(**NOT PROVABLE because no "surjective pairing" for records
-Goalw [Join_def] "Join prgF prgF = prgF";
-auto();
-qed "Join_absorb";
-*)
-
 
 (*
 val field_defs = thms"program.field_defs";
@@ -149,3 +51,124 @@
 val update_convs = thms"program.update_convs";
 val simps = thms"program.simps";
 *)
+
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
+by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "Join_Null";
+*)
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def] "Join prgF prgF = prgF";
+by Auto_tac;
+qed "Join_absorb";
+*)
+
+
+
+(*** Safety: constrains, stable, FP ***)
+
+Goalw [constrains_def, JOIN_def]
+    "constrains (Acts (JN i:I. prg i)) A B = \
+\    (ALL i:I. constrains (Acts (prg i)) A B)";
+by Auto_tac;
+qed "constrains_JN";
+
+(**FAILS, I think; see 5.4.1, Substitution Axiom.
+Goalw [Constrains_def]
+    "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
+by (simp_tac (simpset() addsimps [constrains_JN]) 1);
+by (Blast_tac 1);
+qed "Constrains_JN";
+**)
+
+Goalw [constrains_def, Join_def]
+    "constrains (Acts (Join prgF prgG)) A B =  \
+\    (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
+by (simp_tac (simpset() addsimps [ball_Un]) 1);
+qed "constrains_Join";
+
+Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
+\     ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
+by (simp_tac (simpset() addsimps [constrains_Join]) 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "constrains_Join_weaken";
+
+Goalw [stable_def] 
+    "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
+by (simp_tac (simpset() addsimps [constrains_JN]) 1);
+qed "stable_JN";
+
+Goal "stable (Acts (Join prgF prgG)) A = \
+\     (stable (Acts prgF) A & stable (Acts prgG) A)";
+by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
+qed "stable_Join";
+
+Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
+by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
+qed "FP_JN";
+
+
+(*** Progress: transient, ensures ***)
+
+Goalw [transient_def, JOIN_def]
+   "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
+by (Simp_tac 1);
+qed "transient_JN";
+
+Goalw [transient_def, Join_def]
+   "transient (Acts (Join prgF prgG)) A = \
+\   (transient (Acts prgF) A | transient (Acts prgG) A)";
+by (simp_tac (simpset() addsimps [bex_Un]) 1);
+qed "transient_Join";
+
+Goalw [ensures_def]
+    "ensures (Acts (JN i:I. prg i)) A B = \
+\    ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
+\     (EX i:I. ensures (Acts (prg i)) A B))";
+by (auto_tac (claset(),
+	      simpset() addsimps [constrains_JN, transient_JN]));
+qed "ensures_JN";
+
+Goalw [ensures_def]
+     "ensures (Acts (Join prgF prgG)) A B =     \
+\     (constrains (Acts prgF) (A-B) (A Un B) & \
+\      constrains (Acts prgG) (A-B) (A Un B) & \
+\      (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
+by (auto_tac (claset(),
+	      simpset() addsimps [constrains_Join, transient_Join]));
+qed "ensures_Join";
+
+Goalw [stable_def, constrains_def, Join_def]
+    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  id: Acts prgG |] \
+\    ==> constrains (Acts (Join prgF prgG)) A A'";
+by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
+by (Blast_tac 1);
+qed "stable_constrains_Join";
+
+(*Premises cannot use Invariant because  Stable prgF A  is weaker than
+  stable (Acts prgG) A *)
+Goal  "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
+\      ==> Invariant (Join prgF prgG) A";
+by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
+				  stable_Join]) 1);
+by (force_tac(claset() addIs [stable_reachable, stable_Int],
+	      simpset() addsimps [Acts_Join]) 1);
+qed "stable_Join_Invariant";
+
+Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
+\     ==> ensures (Acts (Join prgF prgG)) A B";
+by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
+by (etac constrains_weaken 1);
+by Auto_tac;
+qed "ensures_stable_Join1";
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
+\     ==> ensures (Acts (Join prgF prgG)) A B";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
+qed "ensures_stable_Join2";
+
diff -r b380921982b9 -r 1861a564d7e2 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Union.thy	Thu Aug 13 18:06:40 1998 +0200
@@ -11,6 +11,9 @@
 Union = SubstAx + FP +
 
 constdefs
+   JOIN  :: ['a set, 'a => 'b program] => 'b program
+    "JOIN I prg == (|Init = INT i:I. Init (prg i),
+	           Acts = UN  i:I. Acts (prg i)|)"
 
    Join :: ['a program, 'a program] => 'a program
     "Join prgF prgG == (|Init = Init prgF Int Init prgG,
@@ -19,4 +22,10 @@
    Null :: 'a program
     "Null == (|Init = UNIV, Acts = {id}|)"
 
+syntax
+  "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
+
+translations
+  "JN x:A. B"   == "JOIN A (%x. B)"
+
 end