# HG changeset patch
# User paulson
# Date 907077527 -7200
# Node ID aad639e56d4eb65bd61b54631060e5d218d7e957
# Parent  d2377657f8efd377f4cba685713b08997a9f1a16
Now id:(Acts prg) is implicit

diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -69,7 +69,7 @@
 
 Goal "[| ALL m. Constrains prg {m} (maxfg m); \
 \               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
-\               n: common;  id: Acts prg |]  \
+\               n: common |]  \
 \            ==> LeadsTo prg (atMost n) common";
 by (rtac LeadsTo_weaken_R 1);
 by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
@@ -82,7 +82,7 @@
 (*The "ALL m: -common" form echoes CMT6.*)
 Goal "[| ALL m. Constrains prg {m} (maxfg m); \
 \               ALL m: -common. LeadsTo prg {m} (greaterThan m); \
-\               n: common;  id: Acts prg |]  \
+\               n: common |]  \
 \            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
 by (rtac lemma 1);
 by (ALLGOALS Asm_simp_tac);
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -89,14 +89,14 @@
 qed "ball_Constrains_INT";
 
 Goalw [Constrains_def]
-     "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
+     "Constrains prg A A' ==> 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);
+by (ALLGOALS
+    (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
 qed "Constrains_imp_subset";
 
 Goalw [Constrains_def]
-    "[| id: Acts prg; Constrains prg A B; Constrains prg B C |]   \
+    "[| 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";
@@ -167,7 +167,7 @@
 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); Constrains prg B B' |] \
 \   ==> Constrains prg A (A' Un B')";
 by (Blast_tac 1);
 qed "Constrains_cancel";
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -20,11 +20,6 @@
 Addsimps [simp_of_set invFG_def];
 
 
-Goalw [Join_def] "id : Acts (Join prgF prgG) ";
-by (Simp_tac 1);
-qed "id_in_Acts";
-AddIffs [id_in_Acts];
-
 Goal "Invariant (Join prgF prgG) invFG";
 by (rtac InvariantI 1);
 by (Force_tac 1);
@@ -59,6 +54,5 @@
 by (rtac lemma2_2 2);
 by (rtac LeadsTo_Trans 1);
 by (rtac lemma2_2 2);
-by (rtac (lemma2_1) 1);
-by Auto_tac;
+by (rtac lemma2_1 1);
 qed "progress";
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Handshake.thy
--- a/src/HOL/UNITY/Handshake.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Handshake.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -22,7 +22,7 @@
 
   prgF :: "state program"
     "prgF == (|Init = {s. NF s = 0 & BB s},
-	       Acts = {id, cmdF}|)"
+	       Acts0 = {cmdF}|)"
 
   (*G's program*)
   cmdG :: "(state*state) set"
@@ -30,7 +30,7 @@
 
   prgG :: "state program"
     "prgG == (|Init = {s. NG s = 0 & BB s},
-	       Acts = {id, cmdG}|)"
+	       Acts0 = {cmdG}|)"
 
   (*the joint invariant*)
   invFG :: "state set"
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Lift.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -118,8 +118,8 @@
     (*for the moment, we OMIT button_press*)
     "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
 		          ~ open s & req s = {}},
-	       Acts = {id, request_act, open_act, close_act,
-		       req_up, req_down, move_up, move_down}|)"
+	       Acts0 = {request_act, open_act, close_act,
+		        req_up, req_down, move_up, move_down}|)"
 
 
   (** Invariants **)
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -63,9 +63,8 @@
 
   Mprg :: state program
     "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0},
-	       Acts = {id,
-	               cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
-	               cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
+	       Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
+	                cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)"
 
 
   (** The correct invariants **)
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/NSP_Bad.thy
--- a/src/HOL/UNITY/NSP_Bad.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -55,6 +55,6 @@
   Nprg :: state program
     (*Initial trace is empty*)
     "Nprg == (|Init = {[]},   
-	       Acts = {id, Fake, NS1, NS2, NS3}|)"
+	       Acts0 = {Fake, NS1, NS2, NS3}|)"
 
 end
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Reach.thy
--- a/src/HOL/UNITY/Reach.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -25,7 +25,7 @@
 
   Rprg :: state program
     "Rprg == (|Init = {%v. v=init},
-	       Acts = insert id (UN (u,v): edges. {asgt u v})|)"
+	       Acts0 = (UN (u,v): edges. {asgt u v})|)"
 
   reach_invariant :: state set
     "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -65,7 +65,7 @@
 
 (*** Derived rules ***)
 
-Goal "id: Acts prg ==> LeadsTo prg A UNIV";
+Goal "LeadsTo prg A UNIV";
 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
 				      Int_lower1 RS subset_imp_leadsTo]) 1);
 qed "LeadsTo_UNIV";
@@ -92,7 +92,7 @@
 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
 qed "LeadsTo_Un";
 
-Goal "[| A <= B;  id: Acts prg |] ==> LeadsTo prg A B";
+Goal "[| A <= B |] ==> LeadsTo prg A B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "subset_imp_LeadsTo";
@@ -105,20 +105,20 @@
 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 |]  \
+Goal "[| LeadsTo prg A A';  B <= A |]  \
 \     ==> 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;   \
+Goal "[| LeadsTo prg A A';   \
 \        B  <= A;   A' <= B' |] \
 \     ==> LeadsTo prg B B'";
 by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
 			       LeadsTo_Trans]) 1);
 qed "LeadsTo_weaken";
 
-Goal "[| reachable prg <= C;  LeadsTo prg A A'; id: Acts prg;   \
+Goal "[| reachable prg <= C;  LeadsTo prg A A';   \
 \        C Int B <= A;   C Int A' <= B' |] \
 \     ==> LeadsTo prg B B'";
 by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
@@ -127,11 +127,11 @@
 
 (** Two theorems for "proof lattices" **)
 
-Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+Goal "[| 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 |] \
+Goal "[| 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);
@@ -140,21 +140,15 @@
 
 (** Distributive laws **)
 
-Goal "id: Acts prg ==> \
-\       LeadsTo prg (A Un B) C  =  \
-\       (LeadsTo prg A C & LeadsTo prg B C)";
+Goal "LeadsTo prg (A Un B) C  = (LeadsTo prg A C & LeadsTo prg B C)";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Un_distrib";
 
-Goal "id: Acts prg ==> \
-\       LeadsTo prg (UN i:I. A i) B  =  \
-\       (ALL i : I. LeadsTo prg (A i) B)";
+Goal "LeadsTo prg (UN i:I. A i) B  =  (ALL i : I. LeadsTo prg (A i) B)";
 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_UN_distrib";
 
-Goal "id: Acts prg ==> \
-\       LeadsTo prg (Union S) B  =  \
-\       (ALL A : S. LeadsTo prg A B)";
+Goal "LeadsTo prg (Union S) B  =  (ALL A : S. LeadsTo prg A B)";
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Union_distrib";
 
@@ -181,7 +175,7 @@
 qed "Invariant_LeadsTo_Basis";
 
 Goal "[| Invariant prg INV;      \
-\        LeadsTo prg A A'; id: Acts prg;   \
+\        LeadsTo prg A A';   \
 \        INV Int B  <= A;  INV Int A' <= B' |] \
 \     ==> LeadsTo prg B B'";
 by (rtac Invariant_LeadsToI 1);
@@ -194,7 +188,7 @@
 
 (*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 (A Int B) C; id: Acts prg |] \
+Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C |] \
 \     ==> LeadsTo prg A C";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
 qed "LeadsTo_Diff";
@@ -236,27 +230,26 @@
 
 (** The cancellation law **)
 
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \
-\        id: Acts prg |]    \
+Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B' |]    \
 \     ==> LeadsTo prg A (A' Un B')";
 by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
 			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
 qed "LeadsTo_cancel2";
 
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B' |] \
 \     ==> LeadsTo prg A (A' Un B')";
 by (rtac LeadsTo_cancel2 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
 qed "LeadsTo_cancel_Diff2";
 
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B' |] \
 \     ==> LeadsTo prg A (B' Un A')";
 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
 qed "LeadsTo_cancel1";
 
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B' |] \
 \     ==> LeadsTo prg A (B' Un A')";
 by (rtac LeadsTo_cancel1 1);
 by (assume_tac 2);
@@ -291,24 +284,23 @@
 qed "PSP_stable2";
 
 Goalw [LeadsTo_def, Constrains_def]
-     "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
+     "[| LeadsTo prg A A'; Constrains prg B B' |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
 by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
 qed "PSP";
 
-Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; Constrains prg B B' |] \
 \     ==> 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 prg B B'; id: Acts prg |] \
+     "[| LeadsTo prg A A'; Unless prg B B' |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
 by (dtac PSP 1);
 by (assume_tac 1);
 by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
-			       subset_imp_LeadsTo]) 2);
-by (assume_tac 1);
+			       subset_imp_LeadsTo]) 1);
 qed "PSP_Unless";
 
 
@@ -317,20 +309,18 @@
 (** Meta or object quantifier ????? **)
 Goal "[| wf r;     \
 \        ALL m. LeadsTo prg (A Int f-``{m})                     \
-\                           ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\        id: Acts prg |] \
+\                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> LeadsTo prg A B";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (etac leadsTo_wf_induct 1);
-by (assume_tac 2);
+by (Simp_tac 2);
 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
 qed "LeadsTo_wf_induct";
 
 
 Goal "[| wf r;     \
 \        ALL m:I. LeadsTo prg (A Int f-``{m})                   \
-\                             ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\        id: Acts prg |] \
+\                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> LeadsTo prg A ((A - (f-``I)) Un B)";
 by (etac LeadsTo_wf_induct 1);
 by Safe_tac;
@@ -341,45 +331,37 @@
 
 
 Goal "[| ALL m. LeadsTo prg (A Int f-``{m})                     \
-\                           ((A Int f-``(lessThan m)) Un B);   \
-\        id: Acts prg |] \
+\                           ((A Int f-``(lessThan m)) Un B) |] \
 \     ==> LeadsTo prg A B";
 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
-by (assume_tac 2);
 by (Asm_simp_tac 1);
 qed "LessThan_induct";
 
 (*Integer version.  Could generalize from #0 to any lower bound*)
-val [reach, prem, id] =
+val [reach, prem] =
 Goal "[| reachable prg <= {s. #0 <= f s};  \
 \        !! z. LeadsTo prg (A Int {s. f s = z})                     \
-\                           ((A Int {s. f s < z}) Un B);   \
-\        id: Acts prg |] \
+\                           ((A Int {s. f s < z}) Un B) |] \
 \     ==> LeadsTo prg A B";
 by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
 by (simp_tac (simpset() addsimps [vimage_def]) 1);
 br ([reach, prem] MRS reachable_LeadsTo_weaken) 1;
-by (auto_tac (claset(),
-	      simpset() addsimps [id, nat_eq_iff, nat_less_iff]));
+by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
 qed "integ_0_le_induct";
 
 Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m})   \
-\                                        ((A Int f-``(lessThan m)) Un B);   \
-\              id: Acts prg |] \
+\                                        ((A Int f-``(lessThan m)) Un B) |] \
 \           ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
 by (rtac (wf_less_than RS Bounded_induct) 1);
-by (assume_tac 2);
 by (Asm_simp_tac 1);
 qed "LessThan_bounded_induct";
 
 Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m})   \
-\                              ((A Int f-``(greaterThan m)) Un B);   \
-\        id: Acts prg |] \
+\                              ((A Int f-``(greaterThan m)) Un B) |] \
 \     ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
-by (assume_tac 2);
 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
 by (Clarify_tac 1);
 by (case_tac "m<l" 1);
@@ -391,14 +373,14 @@
 (*** Completion: Binary and General Finite versions ***)
 
 Goal "[| LeadsTo prg A A';  Stable prg A';   \
-\        LeadsTo prg B B';  Stable prg B';  id: Acts prg |] \
+\        LeadsTo prg B B';  Stable prg B' |] \
 \     ==> LeadsTo prg (A Int B) (A' Int B')";
 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      \
 \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
 \         (ALL i:I. Stable prg (A' i)) -->         \
 \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
@@ -409,8 +391,7 @@
 
 
 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 B (B' Un C);  Constrains prg B' (B' Un C) |] \
 \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
 				       Int_Un_distrib]) 1);
@@ -418,7 +399,7 @@
 qed "Completion";
 
 
-Goal "[| finite I;  id: Acts prg |] \
+Goal "[| finite I |] \
 \     ==> (ALL i:I. LeadsTo 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)";
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -9,6 +9,13 @@
 
 *)
 
+Goal "id: Acts prg";
+by (simp_tac (simpset() addsimps [Acts_def]) 1);
+qed "id_in_Acts";
+AddIffs [id_in_Acts];
+
+
+
 Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
 by Safe_tac;
 by (etac traces.induct 2);
@@ -20,11 +27,12 @@
 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
 qed "stable_reachable";
 
-Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
+Goalw [Acts_def]
+     "(act : Acts(|Init=init, Acts0=acts|)) = (act=id | act : acts)";
 by Auto_tac;
 qed "Acts_eq";
 
-Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
+Goal "(s : Init(|Init=init, Acts0=acts|)) = (s:init)";
 by Auto_tac;
 qed "Init_eq";
 
@@ -34,8 +42,8 @@
 (*** These three rules allow "lazy" definition expansion ***)
 
 val [rew] = goal thy
-    "[| prg == (|Init=init, Acts=acts|) |] \
-\    ==> Init prg = init & Acts prg = acts";
+    "[| prg == (|Init=init, Acts0=acts|) |] \
+\    ==> Init prg = init & Acts prg = insert id acts";
 by (rewtac rew);
 by Auto_tac;
 qed "def_prg_simps";
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -25,8 +25,13 @@
 
 
 record 'a program =
-  Init :: 'a set
-  Acts :: "('a * 'a)set set"
+  Init  :: 'a set
+  Acts0 :: "('a * 'a)set set"
+
+
+constdefs
+    Acts :: "'a program => ('a * 'a)set set"
+    "Acts prg == insert id (Acts0 prg)"
 
 
 consts reachable :: "'a program => 'a set"
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Tue Sep 29 15:58:47 1998 +0200
@@ -14,19 +14,27 @@
 qed "Init_Join";
 
 Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
-by (simp_tac (simpset() addsimps [Join_def]) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [Acts_def, Join_def]));
 qed "Acts_Join";
 
 Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
 by (simp_tac (simpset() addsimps [JOIN_def]) 1);
 qed "Init_JN";
 
-Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
-by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))";
+by (auto_tac (claset(),
+	      simpset() addsimps [Acts_def, JOIN_def]));
 qed "Acts_JN";
 
 Addsimps [Init_Join, Init_JN];
 
+Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)";
+by (simp_tac (simpset() addsimps [Acts_def, JOIN_def, Join_def]) 1);
+qed "JN_insert";
+Addsimps[JN_insert];
+
+
 (** Theoretical issues **)
 
 Goal "Join prgF prgG = Join prgG prgF";
@@ -34,7 +42,7 @@
 qed "Join_commute";
 
 Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
-by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
+by (simp_tac (simpset() addsimps Un_ac@[Join_def, Acts_def, Int_assoc]) 1);
 qed "Join_assoc";
 
 
@@ -50,13 +58,20 @@
 *)
 
 
-(**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, SKIP_def] "Join prgF SKIP = prgF";
+by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "Join_SKIP";
+
+    In order to prove Join_SKIP, we possibly need
+    "Acts0 = ... - {id}" in JOIN_def and Join_def.  But then Join_absorb only
+    holds if id ~: Acts0(prg).  Or else we need to change 'a program to 
+    an abstract type!  Then equality could be made to ignore Acts0.
+
+NOT PROVABLE because no "surjective pairing" for records
 Goalw [Join_def] "Join prgF prgF = prgF";
 by Auto_tac;
 qed "Join_absorb";
@@ -64,10 +79,19 @@
 
 
 
+Goal "(JN G:{}. G) = SKIP";
+by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
+qed "JN_empty";
+Addsimps [JN_empty];
+
+
+
+
 (*** Safety: constrains, stable, FP ***)
 
 Goalw [constrains_def, JOIN_def]
-    "constrains (Acts (JN i:I. prg i)) A B = \
+    "I ~= {} ==> \
+\    constrains (Acts (JN i:I. prg i)) A B = \
 \    (ALL i:I. constrains (Acts (prg i)) A B)";
 by Auto_tac;
 qed "constrains_JN";
@@ -80,10 +104,11 @@
 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);
+Goal "constrains (Acts (Join prgF prgG)) A B =  \
+\     (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
+by (auto_tac
+    (claset(),
+     simpset() addsimps [constrains_def, Join_def, Acts_def, ball_Un]));
 qed "constrains_Join";
 
 Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
@@ -92,9 +117,9 @@
 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);
+Goal "I ~= {} ==> \
+\     stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
+by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
 qed "stable_JN";
 
 Goal "stable (Acts (Join prgF prgG)) A = \
@@ -102,30 +127,32 @@
 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);
+Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
+by (asm_simp_tac (simpset() addsimps [FP_def, 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);
+Goal "I ~= {} ==> \
+\   transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
+by (auto_tac (claset(),
+	      simpset() addsimps [transient_def, JOIN_def]));
 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);
+Goal "transient (Acts (Join prgF prgG)) A = \
+\     (transient (Acts prgF) A | transient (Acts prgG) A)";
+by (auto_tac (claset(),
+	      simpset() addsimps [bex_Un, Acts_def, transient_def,
+				  Join_def]));
 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))";
+Goal "I ~= {} ==> \
+\     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]));
+	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
 qed "ensures_JN";
 
 Goalw [ensures_def]
@@ -146,7 +173,7 @@
 
 (*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 |] \
+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);
diff -r d2377657f8ef -r aad639e56d4e src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:25 1998 +0200
+++ b/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:47 1998 +0200
@@ -12,15 +12,15 @@
 
 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 I prg == (|Init  = INT i:I. Init (prg i),
+	             Acts0 = UN  i:I. Acts (prg i)|)"
 
    Join :: ['a program, 'a program] => 'a program
-    "Join prgF prgG == (|Init = Init prgF Int Init prgG,
-			 Acts = Acts prgF Un Acts prgG|)"
+    "Join prgF prgG == (|Init  = Init prgF Int Init prgG,
+			 Acts0 = Acts prgF Un Acts prgG|)"
 
-   Null :: 'a program
-    "Null == (|Init = UNIV, Acts = {id}|)"
+   SKIP :: 'a program
+    "SKIP == (|Init = UNIV, Acts0 = {}|)"
 
 syntax
   "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)