# HG changeset patch
# User paulson
# Date 910354829 -3600
# Node ID 8e0a4c4fd67baccd5c133a8d0b231530b3cce288
# Parent  06af82bec2f12fb0b08482026bc9d442742243f2
Revising the Client proof as suggested by Michel Charpentier.  New lemmas
about composition (in Union.ML), etc.  Also changed "length" to "size"
because it is displayed as "size" in any event.

diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Client.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -7,19 +7,7 @@
 *)
 
 
-(*Perhaps move to SubstAx.ML*)
-Goal "[| F : Stable A;  F : transient C;  \
-\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
-by (etac reachable_LeadsTo_weaken 1);
-by (rtac LeadsTo_Diff 1);
-by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
-qed "Stable_transient_reachable_LeadsTo";
-
-
-
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
+claset_ref() := claset();
 
 Addsimps [Cli_prg_def RS def_prg_Init];
 program_defs_ref := [Cli_prg_def];
@@ -29,17 +17,6 @@
 (*Simplification for records*)
 Addsimps (thms"state.update_defs");
 
-(*CAN THIS be generalized?
-  Importantly, the second case considers actions that are in G
-  and NOT in Cli_prg (needed to use localTo_imp_equals) *)
-Goal "(act : Acts (Cli_prg Join G)) = \
-\      (act : {Id, rel_act, tok_act, ask_act} | \
-\       act : Acts G & act ~: Acts Cli_prg)";
-by (asm_full_simp_tac (simpset() addsimps [Cli_prg_def, Acts_Join]) 1);
-(*don't unfold definitions of actions*)
-by (blast_tac HOL_cs 1);
-qed "Acts_Cli_Join_eq";
-
 
 fun invariant_tac i = 
     rtac invariantI i  THEN
@@ -73,92 +50,92 @@
 *)
 Goal "Cli_prg:                             \
 \       invariant ({s. tok s <= Max}  Int  \
-\                  {s. ALL n: lessThan (length (ask s)). ask s!n <= Max})";
+\                  {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
 by (invariant_tac 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "ask_bounded";
 
+(** Several facts used to prove Lemma 1 **)
+
+Goal "Cli_prg: stable {s. rel s <= giv s}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_rel_le_giv";
+
+Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_size_rel_le_giv";
+
+Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_size_ask_le_rel";
+
 
 (*We no longer need constrains_tac to expand the program definition, and 
-  expanding it is extremely expensive!  Instead, Acts_Cli_Join_eq expands
-  the program.*)
+  expanding it is extremely expensive!*)
 program_defs_ref := [];
 
 (*Safety property 2: clients return the right number of tokens*)
-Goalw [increasing_def]
-      "Cli_prg : (increasing giv Int (rel localTo Cli_prg))  \
-\                guarantees invariant {s. rel s <= giv s}";
+Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
+\               guarantees Invariant {s. rel s <= giv s}";
 by (rtac guaranteesI 1);
-by (invariant_tac 1);
+by (rtac InvariantI 1);
 by (Force_tac 1);
-by (subgoal_tac "rel s <= giv s'" 1);
-by (force_tac (claset(),
-	       simpset() addsimps [stable_def, constrains_def]) 2);
-by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
-(*we note that "rel" is local to Client*)
-by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
+by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
+			       stable_rel_le_giv]) 1);
 qed "ok_guar_rel_prefix_giv";
 
 
 (*** Towards proving the liveness property ***)
 
 Goal "Cli_prg Join G   \
-\       : transient {s. length (giv s) = Suc k &  \
-\                       length (rel s) = k & ask s ! k <= giv s ! k}";
+\       : transient {s. size (giv s) = Suc k &  \
+\                       size (rel s) = k & ask s ! k <= giv s ! k}";
 by (res_inst_tac [("act", "rel_act")] transient_mem 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
 qed "transient_lemma";
 
+
+
+val rewrite_o = rewrite_rule [o_def];
+
 Goal "Cli_prg : \
-\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
-\                 Int invariant giv_meets_ask) \
-\      guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
-\                               length (rel s) <= length (giv s)}";
+\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
+\      guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \
+\                            {s. size (rel s) <= size (giv s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
-by (dtac (impOfSubs increasing_length) 1);
-by (invariant_tac 1);
- by (Force_tac 1);
-by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
-by Auto_tac;
- by (TRYALL (dtac localTo_imp_equals THEN' atac));
-     by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
-by (force_tac (claset() addD2 ("x",localTo_imp_equals),
-	       simpset() addsimps [increasing_def, Acts_Join, stable_def, 
-				   constrains_def]) 1);
+by (dtac (impOfSubs (rewrite_o Increasing_size)) 1);
+by (rtac InvariantI 1);
+by (Force_tac 1);
+by (rtac Stable_Int 1);
+by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+	               addIs [Increasing_localTo_Stable, 
+			      stable_size_rel_le_giv]) 2);
+by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
+			      stable_size_ask_le_rel]) 1);
 val lemma1 = result();
 
 
 Goal "Cli_prg : \
-\      (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
-\                 Int invariant giv_meets_ask) \
-\      guarantees (LeadsTo {s. k < length (giv s)}    \
-\                          {s. k < length (rel s)})";
+\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\                 Int Invariant giv_meets_ask) \
+\      guarantees (LeadsTo {s. k < size (giv s)}    \
+\                          {s. k < size (rel s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (rtac Stable_transient_reachable_LeadsTo 1);
-  by (res_inst_tac [("k", "k")] transient_lemma 2);
- by (rtac stable_imp_Stable 1);
- by (dtac (impOfSubs increasing_length) 1);
- by (force_tac (claset(),
- 	        simpset() addsimps [increasing_def, 
-				   stable_def, constrains_def]) 1);
-(** LEVEL 7 **)
-(*
- 1. !!G. [| Cli_prg Join G : invariant giv_meets_ask;
-            Cli_prg Join G : ask localTo Cli_prg;
-            Cli_prg Join G : increasing giv;
-            Cli_prg Join G : rel localTo Cli_prg |]
-         ==> reachable (Cli_prg Join G)
-             <= - {s. k < length (giv s)} Un {s. k < length (rel s)} Un
-                {s. length (giv s) = Suc k &
-                    length (rel s) = k & ask s ! k <= giv s ! k}
-x
-*)
+by (res_inst_tac [("k", "k")] transient_lemma 2);
+by (force_tac (claset() addDs [impOfSubs Increasing_size,
+			       impOfSubs Increasing_Stable_less],
+	       simpset()) 1);
 by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
  by (Blast_tac 1);
-by (auto_tac (claset() addSDs [invariant_includes_reachable],
-	      simpset() addsimps [giv_meets_ask_def]));
+by (auto_tac (claset(),
+	      simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
 by (ALLGOALS Force_tac);
 qed "client_correct";
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Client.thy	Fri Nov 06 13:20:29 1998 +0100
@@ -29,9 +29,9 @@
   
   rel_act :: "(state*state) set"
     "rel_act == {(s,s').
-		  EX nrel. nrel = length (rel s) &
+		  EX nrel. nrel = size (rel s) &
 		           s' = s (| rel := rel s @ [giv s!nrel] |) &
-		           nrel < length (giv s) &
+		           nrel < size (giv s) &
 		           ask s!nrel <= giv s!nrel}"
 
   (** Choose a new token requirement **)
@@ -45,7 +45,7 @@
   ask_act :: "(state*state) set"
     "ask_act == {(s,s'). s'=s |
 		         (s' = s (|ask := ask s @ [tok s]|) &
-		          length (ask s) = length (rel s))}"
+		          size (ask s) = size (rel s))}"
 
   Cli_prg :: state program
     "Cli_prg == mk_program ({s. tok s : atMost Max &
@@ -56,7 +56,7 @@
 
   giv_meets_ask :: state set
     "giv_meets_ask ==
-       {s. length (giv s) <= length (ask s) & 
-           (ALL n: lessThan (length (giv s)). ask s!n <= giv s!n)}"
+       {s. size (giv s) <= size (ask s) & 
+           (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
 
 end
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Comp.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -43,6 +43,10 @@
 				      component_Acts, component_Init]) 1);
 qed "component_anti_sym";
 
+Goalw [component_def]
+      "component F H = (EX G. F Join G = H & Disjoint F G)";
+by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
+qed "component_eq";
 
 (*** existential properties ***)
 
@@ -101,8 +105,9 @@
 (*** guarantees ***)
 
 (*This equation is more intuitive than the official definition*)
-Goalw [guarantees_def, component_def]
-      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
+Goal "(F : A guarantees B) = \
+\     (ALL G. F Join G : A & Disjoint F G --> F Join G : B)";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (Blast_tac 1);
 qed "guarantees_eq";
 
@@ -154,13 +159,16 @@
 by (Blast_tac 1);
 qed "ex_guarantees";
 
-val prems = Goalw [guarantees_def, component_def]
-      "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
+val prems = Goal
+     "(!!G. [| F Join G : A;  Disjoint F G |] ==> F Join G : B) \
+\     ==> F : A guarantees B";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
-Goal "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
-by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1);
+Goalw [guarantees_def, component_def]
+     "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
+by (Blast_tac 1);
 qed "guaranteesD";
 
 
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Constrains.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -81,7 +81,7 @@
 by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
 qed "Constrains_Int";
 
-Goal "[| ALL i:I. F : Constrains (A i) (A' i) |]   \
+Goal "ALL i:I. F : Constrains (A i) (A' i)   \
 \     ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)";
 by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
 by (dtac ball_constrains_INT 1);
@@ -140,6 +140,11 @@
 qed "Stable_Constrains_Int";
 
 Goalw [Stable_def]
+    "(ALL i:I. F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
+by (etac ball_Constrains_UN 1);
+qed "ball_Stable_UN";
+
+Goalw [Stable_def]
     "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
 by (etac ball_Constrains_INT 1);
 qed "ball_Stable_INT";
@@ -156,13 +161,13 @@
      "Increasing f <= Increasing (length o f)";
 by Auto_tac;
 by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "Increasing_length";
+qed "Increasing_size";
 
 Goalw [Increasing_def]
      "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
 by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
 by (Blast_tac 1);
-qed "Increasing_less";
+qed "Increasing_Stable_less";
 
 Goalw [increasing_def, Increasing_def]
      "F : increasing f ==> F : Increasing f";
@@ -211,13 +216,7 @@
 bind_thm ("InvariantE", InvariantD RS conjE);
 
 
-(*The set of all reachable states is an Invariant...*)
-Goal "F : Invariant (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!*)
+(*The set of all reachable states is the strongest Invariant*)
 Goal "F : Invariant A ==> reachable F <= A";
 by (full_simp_tac 
     (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
@@ -233,22 +232,33 @@
 qed "invariant_imp_Invariant";
 
 Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
-     "(F : Invariant A) = (F : invariant (reachable F Int A))";
+     "Invariant A = {F. F : invariant (reachable F Int A)}";
 by (blast_tac (claset() addIs reachable.intrs) 1);
 qed "Invariant_eq_invariant_reachable";
 
+(*Invariant is the "always" notion*)
+Goal "Invariant A = {F. reachable F <= A}";
+by (auto_tac (claset() addDs [invariant_includes_reachable],
+	      simpset() addsimps [Int_absorb2, invariant_reachable,
+				  Invariant_eq_invariant_reachable]));
+qed "Invariant_eq_always";
 
 
-Goal "F : Invariant INV ==> reachable F Int INV = reachable F";
-by (dtac Invariant_includes_reachable 1);
-by (Blast_tac 1);
-qed "reachable_Int_INV";
+Goal "Invariant A = (UN I: Pow A. invariant I)";
+by (simp_tac (simpset() addsimps [Invariant_eq_always]) 1);
+by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
+                               stable_reachable,
+			       impOfSubs invariant_includes_reachable]) 1);
+qed "Invariant_eq_UN_invariant";
+
+
+(*** "Constrains" rules involving Invariant ***)
 
 Goal "[| F : Invariant INV;  F : Constrains (INV Int A) A' |]   \
 \     ==> F : Constrains A A'";
 by (asm_full_simp_tac
-    (simpset() addsimps [Constrains_def, reachable_Int_INV,
-			 Int_assoc RS sym]) 1);
+    (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+			 Constrains_def, Int_assoc RS sym]) 1);
 qed "Invariant_ConstrainsI";
 
 (* [| F : Invariant INV; F : Constrains (INV Int A) A |]
@@ -258,8 +268,8 @@
 Goal "[| F : Invariant INV;  F : Constrains A A' |]   \
 \     ==> F : Constrains A (INV Int A')";
 by (asm_full_simp_tac
-    (simpset() addsimps [Constrains_def, reachable_Int_INV,
-			 Int_assoc RS sym]) 1);
+    (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+			 Constrains_def, Int_assoc RS sym]) 1);
 qed "Invariant_ConstrainsD";
 
 bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
@@ -269,8 +279,7 @@
 (** Conjoining Invariants **)
 
 Goal "[| F : Invariant A;  F : Invariant B |] ==> F : Invariant (A Int B)";
-by (auto_tac (claset(),
-	      simpset() addsimps [Invariant_def, Stable_Int]));
+by (auto_tac (claset(), simpset() addsimps [Invariant_eq_always]));
 qed "Invariant_Int";
 
 (*Delete the nearest invariance assumption (which will be the second one
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -294,6 +294,15 @@
 qed "PSP_Unless";
 
 
+Goal "[| F : Stable A;  F : transient C;  \
+\        reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
+by (etac reachable_LeadsTo_weaken 1);
+by (rtac LeadsTo_Diff 1);
+by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+qed "Stable_transient_reachable_LeadsTo";
+
+
 (*** Induction rules ***)
 
 (** Meta or object quantifier ????? **)
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -69,12 +69,6 @@
 by (Blast_tac 1);
 qed "ball_constrains_UN";
 
-Goalw [constrains_def]
-    "[| ALL i. F : constrains (A i) (A' i) |] \
-\    ==> F : constrains (UN i. A i) (UN i. A' i)";
-by (Blast_tac 1);
-qed "all_constrains_UN";
-
 (** Intersection **)
 
 Goalw [constrains_def]
@@ -89,12 +83,6 @@
 by (Blast_tac 1);
 qed "ball_constrains_INT";
 
-Goalw [constrains_def]
-    "[| ALL i. F : constrains (A i) (A' i) |] \
-\    ==> F : constrains (INT i. A i) (INT i. A' i)";
-by (Blast_tac 1);
-qed "all_constrains_INT";
-
 Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
 by (Blast_tac 1);
 qed "constrains_imp_subset";
@@ -116,16 +104,30 @@
 by (assume_tac 1);
 qed "stableD";
 
+(** Union **)
+
 Goalw [stable_def]
     "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
 by (blast_tac (claset() addIs [constrains_Un]) 1);
 qed "stable_Un";
 
 Goalw [stable_def]
+    "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)";
+by (blast_tac (claset() addIs [ball_constrains_UN]) 1);
+qed "ball_stable_UN";
+
+(** Intersection **)
+
+Goalw [stable_def]
     "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
 by (blast_tac (claset() addIs [constrains_Int]) 1);
 qed "stable_Int";
 
+Goalw [stable_def]
+    "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
+by (blast_tac (claset() addIs [ball_constrains_INT]) 1);
+qed "ball_stable_INT";
+
 Goalw [stable_def, constrains_def]
     "[| F : stable C; F : constrains A (C Un A') |]   \
 \    ==> F : constrains (C Un A) (C Un A')";
@@ -150,7 +152,7 @@
 bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
 
 
-(*** invariant & always ***)
+(*** invariant ***)
 
 Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
 by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
@@ -176,17 +178,6 @@
 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
 qed "invariant_includes_reachable";
 
-Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
-by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
-                               stable_reachable,
-			       impOfSubs invariant_includes_reachable]) 1);
-qed "always_eq_UN_invariant";
-
-Goal "F : always A = (EX I. F: invariant I & I <= A)";
-by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
-by (Blast_tac 1);
-qed "always_iff_ex_invariant";
-
 
 (*** increasing ***)
 
@@ -194,13 +185,13 @@
      "increasing f <= increasing (length o f)";
 by Auto_tac;
 by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "increasing_length";
+qed "increasing_size";
 
 Goalw [increasing_def]
      "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
 by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
 by (Blast_tac 1);
-qed "increasing_less";
+qed "increasing_stable_less";
 
 
 (** The Elimination Theorem.  The "free" m has become universally quantified!
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Fri Nov 06 13:20:29 1998 +0100
@@ -24,15 +24,9 @@
   unless :: "['a set, 'a set] => 'a program set"
     "unless A B == constrains (A-B) (A Un B)"
 
-  (*The traditional word for inductive properties.  Anyway, INDUCTIVE is
-    reserved!*)
   invariant :: "'a set => 'a program set"
     "invariant A == {F. Init F <= A} Int stable A"
 
-  (*Safety properties*)
-  always :: "'a set => 'a program set"
-    "always A == {F. reachable F <= A}"
-
   (*Polymorphic in both states and the meaning of <= *)
   increasing :: "['a => 'b::{ord}] => 'a program set"
     "increasing f == INT z. stable {s. z <= f s}"
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Union.ML	Fri Nov 06 13:20:29 1998 +0100
@@ -97,44 +97,6 @@
      simpset() addsimps [constrains_def, Join_def]));
 qed "constrains_Join";
 
-
-(**
-Michel says...
-
-    p inductive-next q' in F
-    p inductive-next q'' in G
-    p noninductive-next q in FoG
-    -------------------------------------------
-    p noninductive-next q /\ (q' \/ q'') in FoG
-
-  From which you deduce:
-
-    inductive-stable A /\ B in F
-    inductive-stable A      in G
-    noninductive-stable B   in FoG
-    ---------------------------------
-    noninductive-stable A /\ B in FoG
-**)
-
-Goal "[| F : constrains A B';  G : constrains A B'';  \
-\        F Join G : Constrains A B |]                 \
-\     ==> F Join G : Constrains A (B Int (B' Un B''))";
-by (auto_tac
-    (claset() addIs [constrains_Int RS constrains_weaken],
-     simpset() addsimps [Constrains_def, constrains_Join]));
-qed "constrains_imp_Join_Constrains";
-
-Goalw [Stable_def, stable_def]
-     "[| F : stable (A Int B);  G : stable A;  \
-\        F Join G : Stable B |]                 \
-\     ==> F Join G : Stable (A Int B)";
-by (auto_tac
-    (claset() addIs [constrains_Int RS constrains_weaken],
-     simpset() addsimps [Constrains_def, constrains_Join]));
-qed "stable_imp_Join_Stable";
-
-
-
 (**FAILS, I think; see 5.4.1, Substitution Axiom.
    The problem is to relate reachable (F Join G) with 
    reachable F and reachable G
@@ -235,12 +197,82 @@
 qed "ensures_stable_Join2";
 
 
-(** localTo **)
+(** Diff and localTo **)
+
+Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "Join_Diff2";
+
+Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
+by Auto_tac;
+qed "Diff_Disjoint";
 
-Goal "[| F Join G : f localTo F;  (s,s') : act;  \
-\        act : Acts G; act ~: Acts F |] ==> f s' = f s";
+Goal "[| F Join G : v localTo F;  Disjoint F G |] \
+\     ==> G : (INT z. stable {s. v s = z})";
 by (asm_full_simp_tac 
-    (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def, 
-			 constrains_def]) 1);
+    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
+			 Acts_Join, stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_stable";
+
+Goal "[| F Join G : v localTo F;  (s,s') : act;  \
+\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
+by (asm_full_simp_tac 
+    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
+			 Acts_Join, stable_def, constrains_def]) 1);
 by (Blast_tac 1);
 qed "localTo_imp_equals";
+
+Goalw [localTo_def, stable_def, constrains_def]
+     "v localTo F <= (f o v) localTo F";
+by (Clarify_tac 1);
+by (auto_tac (claset() addSEs [allE, ballE], simpset()));
+qed "localTo_imp_o_localTo";
+
+
+(*** Higher-level rules involving localTo and Join ***)
+
+Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)};   \
+\        F Join G : v localTo F;       \
+\        F Join G : w localTo F;       \
+\        Disjoint F G |]               \
+\     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
+by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
+by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
+by Auto_tac;
+qed "constrains_localTo_constrains2";
+
+Goalw [stable_def]
+     "[| F : stable {s. P (v s) (w s)};   \
+\        F Join G : v localTo F;       \
+\        F Join G : w localTo F;       \
+\        Disjoint F G |]               \
+\     ==> F Join G : stable {s. P (v s) (w s)}";
+by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
+qed "stable_localTo_stable2";
+
+
+Goal "(UN k. {s. f s = k}) = UNIV";
+by (Blast_tac 1);
+qed "UN_eq_UNIV";
+
+Goal "[| F : stable {s. v s <= w s};   \
+\        F Join G : v localTo F;       \
+\        F Join G : Increasing w;      \
+\        Disjoint F G |]               \
+\     ==> F Join G : Stable {s. v s <= w s}";
+by (safe_tac (claset() addSDs [localTo_imp_stable]));
+by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
+by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
+by (dtac ball_Constrains_UN 1);
+by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
+by (rtac ballI 1);
+by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
+\                                      ({s. v s = k} Un {s. v s <= w s})" 1);
+by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
+by (blast_tac (claset() addIs [constrains_weaken]) 2);
+by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
+by (etac Constrains_weaken 2);
+by Auto_tac;
+qed "Increasing_localTo_Stable";
diff -r 06af82bec2f1 -r 8e0a4c4fd67b src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Union.thy	Fri Nov 06 13:20:29 1998 +0100
@@ -5,7 +5,7 @@
 
 Unions of programs
 
-From Misra's Chapter 5: Asynchronous Compositions of Programs
+Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
 *)
 
 Union = SubstAx + FP +
@@ -23,9 +23,13 @@
   Diff :: "['a program, ('a * 'a)set set] => 'a program"
     "Diff F acts == mk_program (Init F, Acts F - acts)"
 
-  (*The set of systems that regard "f" as local to F*)
+  (*The set of systems that regard "v" as local to F*)
   localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
-    "f localTo F == {G. ALL z. Diff G (Acts F) : stable {s. f s = z}}"
+    "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
+
+  (*Two programs with disjoint actions, except for Id (idling)*)
+  Disjoint :: ['a program, 'a program] => bool
+    "Disjoint F G == Acts F Int Acts G <= {Id}"
 
 syntax
   "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)