# HG changeset patch
# User paulson
# Date 907749120 -7200
# Node ID 3ac11c4af76ae009e6a95728a727ccba75aced2e
# Parent  76a8c72e3fd499864fed817b5790e1740dc3a81b
tidying and renaming

diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -11,8 +11,8 @@
 *)
 
 (*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
-\     ==> Stable prg (atMost n)";
+Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \
+\     ==> Stable F (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,
@@ -21,9 +21,9 @@
 by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
 qed "common_stable";
 
-Goal "[| Init prg <= atMost n;  \
-\        ALL m. Constrains prg {m} (maxfg m); n: common |] \
-\     ==> Invariant prg (atMost n)";
+Goal "[| Init F <= atMost n;  \
+\        ALL m. Constrains F {m} (maxfg m); n: common |] \
+\     ==> Invariant F (atMost n)";
 by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
 qed "common_Invariant";
 
@@ -67,10 +67,10 @@
 
 Addsimps [atMost_Int_atLeast];
 
-Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
+Goal "[| ALL m. Constrains F {m} (maxfg m); \
+\               ALL m: lessThan n. LeadsTo F {m} (greaterThan m); \
 \               n: common |]  \
-\            ==> LeadsTo prg (atMost n) common";
+\            ==> LeadsTo F (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);
@@ -80,10 +80,10 @@
 val lemma = result();
 
 (*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\               ALL m: -common. LeadsTo prg {m} (greaterThan m); \
+Goal "[| ALL m. Constrains F {m} (maxfg m); \
+\               ALL m: -common. LeadsTo F {m} (greaterThan m); \
 \               n: common |]  \
-\            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
+\            ==> LeadsTo F (atMost (LEAST n. n: common)) common";
 by (rtac lemma 1);
 by (ALLGOALS Asm_simp_tac);
 by (etac LeastI 2);
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -32,15 +32,15 @@
 
 Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
 by Auto_tac;
-qed "componet_Acts";
+qed "component_Acts";
 
 Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
 by Auto_tac;
-qed "componet_Init";
+qed "component_Init";
 
 Goal "[| component F G; component G F |] ==> F=G";
 by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
-				      componet_Acts, componet_Init]) 1);
+				      component_Acts, component_Init]) 1);
 qed "component_anti_sym";
 
 
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -13,61 +13,61 @@
 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')*)
+(*constrains (Acts F) B B'
+  ==> constrains (Acts F) (reachable F Int B) (reachable F 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'";
+    "constrains (Acts F) A A' ==> Constrains F 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'";
+    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
+\    ==> Constrains F 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";
+Goalw [Constrains_def, constrains_def] "Constrains F {} B";
 by (Blast_tac 1);
 qed "Constrains_empty";
 
-Goal "Constrains prg A UNIV";
+Goal "Constrains F 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'";
+    "[| Constrains F A A'; A'<=B' |] ==> Constrains F 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'";
+    "[| Constrains F A A'; B<=A |] ==> Constrains F 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'";
+   "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F 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')";
+    "[| Constrains F A A'; Constrains F B B' |]   \
+\    ==> Constrains F (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)";
+    "ALL i:I. Constrains F (A i) (A' i) \
+\    ==> Constrains F (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";
@@ -75,75 +75,75 @@
 (** Intersection **)
 
 Goalw [Constrains_def]
-    "[| Constrains prg A A'; Constrains prg B B' |]   \
-\    ==> Constrains prg (A Int B) (A' Int B')";
+    "[| Constrains F A A'; Constrains F B B' |]   \
+\    ==> Constrains F (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)";
+    "[| ALL i:I. Constrains F (A i) (A' i) |]   \
+\    ==> Constrains F (INT i:I. A i) (INT i:I. A' i)";
 by (dtac ball_constrains_INT 1);
 by (dtac constrains_reachable_Int 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "ball_Constrains_INT";
 
 Goalw [Constrains_def]
-     "Constrains prg A A' ==> reachable prg Int A <= A'";
+     "Constrains F A A' ==> reachable F Int A <= A'";
 by (dtac constrains_imp_subset 1);
 by (ALLGOALS
     (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
 qed "Constrains_imp_subset";
 
 Goalw [Constrains_def]
-    "[| Constrains prg A B; Constrains prg B C |]   \
-\    ==> Constrains prg A C";
+    "[| Constrains F A B; Constrains F B C |]   \
+\    ==> Constrains F 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)";
+Goal "Stable F A = stable (Acts F) (reachable F 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";
+Goalw [Stable_def] "Constrains F A A ==> Stable F A";
 by (assume_tac 1);
 qed "StableI";
 
-Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
+Goalw [Stable_def] "Stable F A ==> Constrains F A A";
 by (assume_tac 1);
 qed "StableD";
 
 Goalw [Stable_def]
-    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
+    "[| Stable F A; Stable F A' |] ==> Stable F (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')";
+    "[| Stable F A; Stable F A' |] ==> Stable F (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')";
+    "[| Stable F C; Constrains F A (C Un A') |]   \
+\    ==> Constrains F (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')";
+    "[| Stable F C; Constrains F (C Int A) A' |]   \
+\    ==> Constrains F (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)";
+    "(ALL i:I. Stable F (A i)) ==> Stable F (INT i:I. A i)";
 by (etac ball_Constrains_INT 1);
 qed "ball_Stable_INT";
 
-Goal "Stable prg (reachable prg)";
+Goal "Stable F (reachable F)";
 by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
 qed "Stable_reachable";
 
@@ -154,34 +154,34 @@
      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)";
+    "[| ALL m. Constrains F {s. s x = m} (B m) |] \
+\    ==> Constrains F {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)";
+    "(ALL m. Constrains F {m} (B m)) ==> Constrains F 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' |] \
-\   ==> Constrains prg A (A' Un B')";
+   "[| Constrains F A (A' Un B); Constrains F B B' |] \
+\   ==> Constrains F A (A' Un B')";
 by (Blast_tac 1);
 qed "Constrains_cancel";
 
 
 (*** Specialized laws for handling Invariants ***)
 
-(** Natural deduction rules for "Invariant prg A" **)
+(** Natural deduction rules for "Invariant F A" **)
 
-Goal "[| Init prg<=A;  Stable prg A |] ==> Invariant prg A";
+Goal "[| Init F<=A;  Stable F A |] ==> Invariant F A";
 by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
 qed "InvariantI";
 
-Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
+Goal "Invariant F A ==> Init F<=A & Stable F A";
 by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
 qed "InvariantD";
 
@@ -189,13 +189,13 @@
 
 
 (*The set of all reachable states is an Invariant...*)
-Goal "Invariant prg (reachable prg)";
+Goal "Invariant F (reachable F)";
 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";
+Goal "Invariant F A ==> reachable F <= A";
 by (full_simp_tac 
     (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
 			 Invariant_def]) 1);
@@ -205,24 +205,24 @@
 qed "Invariant_includes_reachable";
 
 
-Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
+Goal "Invariant F INV ==> reachable F Int INV = reachable F";
 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'";
+Goal "[| Invariant F INV;  Constrains F (INV Int A) A' |]   \
+\     ==> Constrains F A A'";
 by (asm_full_simp_tac
     (simpset() addsimps [Constrains_def, reachable_Int_INV,
 			 Int_assoc RS sym]) 1);
 qed "Invariant_ConstrainsI";
 
-(* [| Invariant prg INV; Constrains prg (INV Int A) A |]
-   ==> Stable prg A *)
+(* [| Invariant F INV; Constrains F (INV Int A) A |]
+   ==> Stable F A *)
 bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
 
-Goal "[| Invariant prg INV;  Constrains prg A A' |]   \
-\     ==> Constrains prg A (INV Int A')";
+Goal "[| Invariant F INV;  Constrains F A A' |]   \
+\     ==> Constrains F A (INV Int A')";
 by (asm_full_simp_tac
     (simpset() addsimps [Constrains_def, reachable_Int_INV,
 			 Int_assoc RS sym]) 1);
@@ -234,7 +234,7 @@
 
 (** Conjoining Invariants **)
 
-Goal "[| Invariant prg A;  Invariant prg B |] ==> Invariant prg (A Int B)";
+Goal "[| Invariant F A;  Invariant F B |] ==> Invariant F (A Int B)";
 by (auto_tac (claset(),
 	      simpset() addsimps [Invariant_def, Stable_Int]));
 qed "Invariant_Int";
@@ -261,7 +261,7 @@
 				   constrains_imp_Constrains] 1),
 	      rtac constrainsI 1,
 	      Full_simp_tac 1,
-	      REPEAT_FIRST (etac disjE),
+	      REPEAT (FIRSTGOAL (etac disjE)),
 	      ALLGOALS Clarify_tac,
 	      ALLGOALS Asm_full_simp_tac]);
 
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Wed Oct 07 10:32:00 1998 +0200
@@ -11,18 +11,18 @@
 constdefs
 
   Constrains :: "['a program, 'a set, 'a set] => bool"
-    "Constrains prg A B == 
-		 constrains (Acts prg)
-                            (reachable prg  Int  A)
-  		            (reachable prg  Int  B)"
+    "Constrains F A B == 
+		 constrains (Acts F)
+                            (reachable F  Int  A)
+  		            (reachable F  Int  B)"
 
   Stable     :: "'a program => 'a set => bool"
-    "Stable prg A == Constrains prg A A"
+    "Stable F A == Constrains F A A"
 
   Unless :: "['a program, 'a set, 'a set] => bool"
-    "Unless prg A B == Constrains prg (A-B) (A Un B)"
+    "Unless F A B == Constrains F (A-B) (A Un B)"
 
   Invariant :: "['a program, 'a set] => bool"
-  "Invariant prg A == (Init prg) <= A & Stable prg A"
+  "Invariant F A == (Init F) <= A & Stable F A"
 
 end
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -71,7 +71,7 @@
 by (exhaust_tac "na" 1);
 by (exhaust_tac "nat" 2);
 by (exhaust_tac "n" 3);
-auto();
+by Auto_tac;
 qed "eq_123";
 
 
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -21,6 +21,12 @@
 time_use_thy "Reach";
 time_use_thy "Handshake";
 time_use_thy "Lift";
+time_use_thy "Comp";
 
-loadpath := "../Auth" :: !loadpath;  (*necessary to find the Auth theories*)
+loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
 use_thy"NSP_Bad";
+
+(*
+loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
+use_thy"Client";
+*)
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -15,14 +15,14 @@
 
 (** Conjoining a safety property **)
 
-Goal "[| reachable prg <= C;  LeadsTo prg (C Int A) A' |]   \
-\     ==> LeadsTo prg A A'";
+Goal "[| reachable F <= C;  LeadsTo F (C Int A) A' |]   \
+\     ==> LeadsTo F A A'";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
 qed "reachable_LeadsToI";
 
-Goal "[| reachable prg <= C;  LeadsTo prg A A' |]   \
-\     ==> LeadsTo prg A (C Int A')";
+Goal "[| reachable F <= C;  LeadsTo F A A' |]   \
+\     ==> LeadsTo F A (C Int A')";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_def, Int_absorb2,
 			 Int_assoc RS sym]) 1);
@@ -31,11 +31,11 @@
 
 (** Conjoining an invariant **)
 
-(* [| Invariant prg C; LeadsTo prg (C Int A) A' |] ==> LeadsTo prg A A' *)
+(* [| Invariant F C; LeadsTo F (C Int A) A' |] ==> LeadsTo F A A' *)
 bind_thm ("Invariant_LeadsToI", 
 	  Invariant_includes_reachable RS reachable_LeadsToI);
 
-(* [| Invariant prg C; LeadsTo prg A A' |] ==> LeadsTo prg A (C Int A') *)
+(* [| Invariant F C; LeadsTo F A A' |] ==> LeadsTo F A (C Int A') *)
 bind_thm ("Invariant_LeadsToD", 
 	  Invariant_includes_reachable RS reachable_LeadsToD);
 
@@ -44,18 +44,18 @@
 
 (*** Introduction rules: Basis, Trans, Union ***)
 
-Goal "leadsTo (Acts prg) A B ==> LeadsTo prg A B";
+Goal "leadsTo (Acts F) A B ==> LeadsTo F A B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
 qed "leadsTo_imp_LeadsTo";
 
-Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] ==> LeadsTo prg A C";
+Goal "[| LeadsTo F A B;  LeadsTo F B C |] ==> LeadsTo F A C";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "LeadsTo_Trans";
 
 val [prem] = Goalw [LeadsTo_def]
- "(!!A. A : S ==> LeadsTo prg A B) ==> LeadsTo prg (Union S) B";
+ "(!!A. A : S ==> LeadsTo F A B) ==> LeadsTo F (Union S) B";
 by (Simp_tac 1);
 by (stac Int_Union 1);
 by (blast_tac (claset() addIs [leadsTo_UN,
@@ -65,34 +65,34 @@
 
 (*** Derived rules ***)
 
-Goal "LeadsTo prg A UNIV";
+Goal "LeadsTo F A UNIV";
 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
 				      Int_lower1 RS subset_imp_leadsTo]) 1);
 qed "LeadsTo_UNIV";
 Addsimps [LeadsTo_UNIV];
 
 (*Useful with cancellation, disjunction*)
-Goal "LeadsTo prg A (A' Un A') ==> LeadsTo prg A A'";
+Goal "LeadsTo F A (A' Un A') ==> LeadsTo F A A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "LeadsTo_Un_duplicate";
 
-Goal "LeadsTo prg A (A' Un C Un C) ==> LeadsTo prg A (A' Un C)";
+Goal "LeadsTo F A (A' Un C Un C) ==> LeadsTo F A (A' Un C)";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "LeadsTo_Un_duplicate2";
 
 val prems = 
-Goal "(!!i. i : I ==> LeadsTo prg (A i) B) ==> LeadsTo prg (UN i:I. A i) B";
+Goal "(!!i. i : I ==> LeadsTo F (A i) B) ==> LeadsTo F (UN i:I. A i) B";
 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
 qed "LeadsTo_UN";
 
 (*Binary union introduction rule*)
-Goal "[| LeadsTo prg A C; LeadsTo prg B C |] ==> LeadsTo prg (A Un B) C";
+Goal "[| LeadsTo F A C; LeadsTo F B C |] ==> LeadsTo F (A Un B) C";
 by (stac Un_eq_Union 1);
 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
 qed "LeadsTo_Un";
 
-Goal "[| A <= B |] ==> LeadsTo prg A B";
+Goal "[| A <= B |] ==> LeadsTo F A B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "subset_imp_LeadsTo";
@@ -100,39 +100,39 @@
 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
 Addsimps [empty_LeadsTo];
 
-Goal "[| LeadsTo prg A A';  A' <= B' |] ==> LeadsTo prg A B'";
+Goal "[| LeadsTo F A A';  A' <= B' |] ==> LeadsTo F A B'";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
 qed_spec_mp "LeadsTo_weaken_R";
 
-Goal "[| LeadsTo prg A A';  B <= A |]  \
-\     ==> LeadsTo prg B A'";
+Goal "[| LeadsTo F A A';  B <= A |]  \
+\     ==> LeadsTo F 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';   \
+Goal "[| LeadsTo F A A';   \
 \        B  <= A;   A' <= B' |] \
-\     ==> LeadsTo prg B B'";
+\     ==> LeadsTo F 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';   \
+Goal "[| reachable F <= C;  LeadsTo F A A';   \
 \        C Int B <= A;   C Int A' <= B' |] \
-\     ==> LeadsTo prg B B'";
+\     ==> LeadsTo F B B'";
 by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
                         addIs [reachable_LeadsToD]) 1);
 qed "reachable_LeadsTo_weaken";
 
 (** Two theorems for "proof lattices" **)
 
-Goal "[| LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+Goal "[| LeadsTo F A B |] ==> LeadsTo F (A Un B) B";
 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
 qed "LeadsTo_Un_post";
 
-Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] \
-\     ==> LeadsTo prg (A Un B) C";
+Goal "[| LeadsTo F A B;  LeadsTo F B C |] \
+\     ==> LeadsTo F (A Un B) C";
 by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
 			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
 qed "LeadsTo_Trans_Un";
@@ -140,33 +140,33 @@
 
 (** Distributive laws **)
 
-Goal "LeadsTo prg (A Un B) C  = (LeadsTo prg A C & LeadsTo prg B C)";
+Goal "LeadsTo F (A Un B) C  = (LeadsTo F A C & LeadsTo F B C)";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Un_distrib";
 
-Goal "LeadsTo prg (UN i:I. A i) B  =  (ALL i : I. LeadsTo prg (A i) B)";
+Goal "LeadsTo F (UN i:I. A i) B  =  (ALL i : I. LeadsTo F (A i) B)";
 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_UN_distrib";
 
-Goal "LeadsTo prg (Union S) B  =  (ALL A : S. LeadsTo prg A B)";
+Goal "LeadsTo F (Union S) B  =  (ALL A : S. LeadsTo F A B)";
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Union_distrib";
 
 
-(** More rules using the premise "Invariant prg" **)
+(** More rules using the premise "Invariant F" **)
 
 Goalw [LeadsTo_def, Constrains_def]
-     "[| Constrains prg (A-A') (A Un A'); transient  (Acts prg) (A-A') |]   \
-\     ==> LeadsTo prg A A'";
+     "[| Constrains F (A-A') (A Un A'); transient  (Acts F) (A-A') |]   \
+\     ==> LeadsTo F 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'";
+Goal "[| Invariant F INV;      \
+\        Constrains F (INV Int (A-A')) (A Un A'); \
+\        transient  (Acts F) (INV Int (A-A')) |]   \
+\ ==> LeadsTo F A A'";
 by (rtac Invariant_LeadsToI 1);
 by (assume_tac 1);
 by (rtac LeadsTo_Basis 1);
@@ -174,10 +174,10 @@
 by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
 qed "Invariant_LeadsTo_Basis";
 
-Goal "[| Invariant prg INV;      \
-\        LeadsTo prg A A';   \
+Goal "[| Invariant F INV;      \
+\        LeadsTo F A A';   \
 \        INV Int B  <= A;  INV Int A' <= B' |] \
-\     ==> LeadsTo prg B B'";
+\     ==> LeadsTo F B B'";
 by (rtac Invariant_LeadsToI 1);
 by (assume_tac 1);
 by (dtac Invariant_LeadsToD 1);
@@ -188,8 +188,8 @@
 
 (*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 |] \
-\     ==> LeadsTo prg A C";
+Goal "[| LeadsTo F (A-B) C; LeadsTo F (A Int B) C |] \
+\     ==> LeadsTo F A C";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
 qed "LeadsTo_Diff";
 
@@ -197,8 +197,8 @@
 
 
 val prems = 
-Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
-\     ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
+Goal "(!! i. i:I ==> LeadsTo F (A i) (A' i)) \
+\     ==> LeadsTo F (UN i:I. A i) (UN i:I. A' i)";
 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
                         addIs prems) 1);
@@ -207,22 +207,22 @@
 
 (*Version with no index set*)
 val prems = 
-Goal "(!! i. LeadsTo prg (A i) (A' i)) \
-\     ==> LeadsTo prg (UN i. A i) (UN i. A' i)";
+Goal "(!! i. LeadsTo F (A i) (A' i)) \
+\     ==> LeadsTo F (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
                         addIs prems) 1);
 qed "LeadsTo_UN_UN_noindex";
 
 (*Version with no index set*)
-Goal "ALL i. LeadsTo prg (A i) (A' i) \
-\     ==> LeadsTo prg (UN i. A i) (UN i. A' i)";
+Goal "ALL i. LeadsTo F (A i) (A' i) \
+\     ==> LeadsTo F (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
 qed "all_LeadsTo_UN_UN";
 
 
 (*Binary union version*)
-Goal "[| LeadsTo prg A A'; LeadsTo prg B B' |] \
-\           ==> LeadsTo prg (A Un B) (A' Un B')";
+Goal "[| LeadsTo F A A'; LeadsTo F B B' |] \
+\           ==> LeadsTo F (A Un B) (A' Un B')";
 by (blast_tac (claset() addIs [LeadsTo_Un, 
 			       LeadsTo_weaken_R]) 1);
 qed "LeadsTo_Un_Un";
@@ -230,27 +230,27 @@
 
 (** The cancellation law **)
 
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B' |]    \
-\     ==> LeadsTo prg A (A' Un B')";
+Goal "[| LeadsTo F A (A' Un B); LeadsTo F B B' |]    \
+\     ==> LeadsTo F 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' |] \
-\     ==> LeadsTo prg A (A' Un B')";
+Goal "[| LeadsTo F A (A' Un B); LeadsTo F (B-A') B' |] \
+\     ==> LeadsTo F 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' |] \
-\     ==> LeadsTo prg A (B' Un A')";
+Goal "[| LeadsTo F A (B Un A'); LeadsTo F B B' |] \
+\     ==> LeadsTo F 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' |] \
-\     ==> LeadsTo prg A (B' Un A')";
+Goal "[| LeadsTo F A (B Un A'); LeadsTo F (B-A') B' |] \
+\     ==> LeadsTo F A (B' Un A')";
 by (rtac LeadsTo_cancel1 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
@@ -261,7 +261,7 @@
 (** The impossibility law **)
 
 (*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "LeadsTo prg A {} ==> reachable prg Int A = {}";
+Goal "LeadsTo F A {} ==> reachable F Int A = {}";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (etac leadsTo_empty 1);
 qed "LeadsTo_empty";
@@ -271,32 +271,32 @@
 
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
 Goal
-  "[| LeadsTo prg A A';  Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
+  "[| LeadsTo F A A';  Stable F B |] ==> LeadsTo F (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 prg B |] \
-\     ==> LeadsTo prg (B Int A) (B Int A')";
+Goal "[| LeadsTo F A A'; Stable F B |] \
+\     ==> LeadsTo F (B Int A) (B Int A')";
 by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
 qed "PSP_stable2";
 
 Goalw [LeadsTo_def, Constrains_def]
-     "[| LeadsTo prg A A'; Constrains prg B B' |] \
-\     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
+     "[| LeadsTo F A A'; Constrains F B B' |] \
+\     ==> LeadsTo F (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' |] \
-\     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| LeadsTo F A A'; Constrains F B B' |] \
+\     ==> LeadsTo F (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' |] \
-\     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
+     "[| LeadsTo F A A'; Unless F B B' |] \
+\     ==> LeadsTo F (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, 
@@ -308,9 +308,9 @@
 
 (** Meta or object quantifier ????? **)
 Goal "[| wf r;     \
-\        ALL m. LeadsTo prg (A Int f-``{m})                     \
+\        ALL m. LeadsTo F (A Int f-``{m})                     \
 \                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\     ==> LeadsTo prg A B";
+\     ==> LeadsTo F A B";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (etac leadsTo_wf_induct 1);
 by (Simp_tac 2);
@@ -319,9 +319,9 @@
 
 
 Goal "[| wf r;     \
-\        ALL m:I. LeadsTo prg (A Int f-``{m})                   \
+\        ALL m:I. LeadsTo F (A Int f-``{m})                   \
 \                             ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\     ==> LeadsTo prg A ((A - (f-``I)) Un B)";
+\     ==> LeadsTo F A ((A - (f-``I)) Un B)";
 by (etac LeadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -330,36 +330,36 @@
 qed "Bounded_induct";
 
 
-Goal "[| ALL m. LeadsTo prg (A Int f-``{m})                     \
+Goal "[| ALL m. LeadsTo F (A Int f-``{m})                     \
 \                           ((A Int f-``(lessThan m)) Un B) |] \
-\     ==> LeadsTo prg A B";
+\     ==> LeadsTo F A B";
 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
 by (Asm_simp_tac 1);
 qed "LessThan_induct";
 
 (*Integer version.  Could generalize from #0 to any lower bound*)
 val [reach, prem] =
-Goal "[| reachable prg <= {s. #0 <= f s};  \
-\        !! z. LeadsTo prg (A Int {s. f s = z})                     \
+Goal "[| reachable F <= {s. #0 <= f s};  \
+\        !! z. LeadsTo F (A Int {s. f s = z})                     \
 \                           ((A Int {s. f s < z}) Un B) |] \
-\     ==> LeadsTo prg A B";
+\     ==> LeadsTo F 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 (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1);
 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})   \
+Goal "[| ALL m:(greaterThan l). LeadsTo F (A Int f-``{m})   \
 \                                        ((A Int f-``(lessThan m)) Un B) |] \
-\           ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
+\           ==> LeadsTo F 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 (Asm_simp_tac 1);
 qed "LessThan_bounded_induct";
 
-Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m})   \
+Goal "[| ALL m:(lessThan l). LeadsTo F (A Int f-``{m})   \
 \                              ((A Int f-``(greaterThan m)) Un B) |] \
-\     ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
+\     ==> LeadsTo F 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 (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
@@ -372,27 +372,27 @@
 
 (*** Completion: Binary and General Finite versions ***)
 
-Goal "[| LeadsTo prg A A';  Stable prg A';   \
-\        LeadsTo prg B B';  Stable prg B' |] \
-\     ==> LeadsTo prg (A Int B) (A' Int B')";
+Goal "[| LeadsTo F A A';  Stable F A';   \
+\        LeadsTo F B B';  Stable F B' |] \
+\     ==> LeadsTo F (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      \
-\     ==> (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)";
+\     ==> (ALL i:I. LeadsTo F (A i) (A' i)) -->  \
+\         (ALL i:I. Stable F (A' i)) -->         \
+\         LeadsTo F (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, ball_Stable_INT]) 1);
 qed_spec_mp "Finite_stable_completion";
 
 
-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) |] \
-\     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
+Goal "[| LeadsTo F A (A' Un C);  Constrains F A' (A' Un C); \
+\        LeadsTo F B (B' Un C);  Constrains F B' (B' Un C) |] \
+\     ==> LeadsTo F (A Int B) ((A' Int B') Un C)";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
 				       Int_Un_distrib]) 1);
 by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
@@ -400,9 +400,9 @@
 
 
 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)";
+\     ==> (ALL i:I. LeadsTo F (A i) (A' i Un C)) -->  \
+\         (ALL i:I. Constrains F (A' i) (A' i Un C)) --> \
+\         LeadsTo F (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);
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:32:00 1998 +0200
@@ -11,8 +11,8 @@
 constdefs
 
    LeadsTo :: "['a program, 'a set, 'a set] => bool"
-    "LeadsTo prg A B ==
-		 leadsTo (Acts prg)
-                         (reachable prg  Int  A)
-  		         (reachable prg  Int  B)"
+    "LeadsTo F A B ==
+		 leadsTo (Acts F)
+                         (reachable F  Int  A)
+  		         (reachable F  Int  B)"
 end
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -17,8 +17,8 @@
 		 Rep_Program_inverse, Abs_Program_inverse];
 
 
-Goal "Id: Acts prg";
-by (cut_inst_tac [("x", "prg")] Rep_Program 1);
+Goal "Id: Acts F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
 by (auto_tac (claset(), rep_ss));
 qed "Id_in_Acts";
 AddIffs [Id_in_Acts];
@@ -35,8 +35,8 @@
 Addsimps [Acts_eq, Init_eq];
 
 
-Goal "[| Init prg = Init prg'; Acts prg = Acts prg' |] ==> prg = prg'";
-by (cut_inst_tac [("p", "Rep_Program prg")] surjective_pairing 1);
+Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1);
 by (auto_tac (claset(), rep_ss));
 by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1);
 by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
@@ -46,8 +46,8 @@
 (*** These three rules allow "lazy" definition expansion ***)
 
 val [rew] = goal thy
-    "[| prg == mk_program (init,acts) |] \
-\    ==> Init prg = init & Acts prg = insert Id acts";
+    "[| F == mk_program (init,acts) |] \
+\    ==> Init F = init & Acts F = insert Id acts";
 by (rewtac rew);
 by Auto_tac;
 qed "def_prg_simps";
@@ -71,13 +71,17 @@
 
 (*** traces and reachable ***)
 
-Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
+Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
 by Safe_tac;
 by (etac traces.induct 2);
 by (etac reachable.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
+by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
 qed "reachable_equiv_traces";
 
-Goal "acts <= Acts prg ==> stable acts (reachable prg)";
-by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
+Goal "Init F <= reachable F";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_subset_reachable";
+
+Goal "acts <= Acts F ==> stable acts (reachable F)";
+by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
 qed "stable_reachable";
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy	Wed Oct 07 10:32:00 1998 +0200
@@ -32,19 +32,19 @@
     "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
 
     Init :: "'a program => 'a set"
-    "Init prg == fst (Rep_Program prg)"
+    "Init F == fst (Rep_Program F)"
 
     Acts :: "'a program => ('a * 'a)set set"
-    "Acts prg == snd (Rep_Program prg)"
+    "Acts F == snd (Rep_Program F)"
 
 
 consts reachable :: "'a program => 'a set"
 
-inductive "reachable prg"
+inductive "reachable F"
   intrs 
-    Init  "s: Init prg ==> s : reachable prg"
+    Init  "s: Init F ==> s : reachable F"
 
-    Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
-	   ==> s' : reachable prg"
+    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
+	   ==> s' : reachable F"
 
 end
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -85,20 +85,29 @@
 by (Blast_tac 1);
 qed "constrains_JN";
 
+Goal "constrains (Acts (F Join G)) A B =  \
+\     (constrains (Acts F) A B & constrains (Acts G) A B)";
+by (auto_tac
+    (claset(),
+     simpset() addsimps [constrains_def, Join_def]));
+qed "constrains_Join";
+
 (**FAILS, I think; see 5.4.1, Substitution Axiom.
+   The problem is to relate reachable (F Join G) with 
+   reachable F and reachable G
+
 Goalw [Constrains_def]
     "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
 by (simp_tac (simpset() addsimps [constrains_JN]) 1);
 by (Blast_tac 1);
 qed "Constrains_JN";
-**)
 
-Goal "constrains (Acts (F Join G)) A B =  \
-\     (constrains (Acts F) A B & constrains (Acts G) A B)";
+Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)";
 by (auto_tac
     (claset(),
-     simpset() addsimps [constrains_def, Join_def, ball_Un]));
-qed "constrains_Join";
+     simpset() addsimps [Constrains_def, constrains_Join]));
+qed "Constrains_Join";
+**)
 
 Goal "[| constrains (Acts F) A A';  constrains (Acts G) B B' |] \
 \     ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')";
diff -r 76a8c72e3fd4 -r 3ac11c4af76a src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Wed Oct 07 10:32:00 1998 +0200
@@ -434,7 +434,7 @@
 \      constrains acts (A1 - B) (A1 Un B); \
 \      constrains acts (A2 - C) (A2 Un C) |] \
 \   ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
-by(Blast_tac 1);
+by (Blast_tac 1);
 val lemma1 = result();