# HG changeset patch
# User paulson
# Date 950883644 -3600
# Node ID 9be357df93d465487432c2850c02bdddbd1429fa
# Parent  f4029c34adef3e4369c6da6bf03e098c0aa6c606
New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.

diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -425,8 +425,8 @@
 	   Client_component_System] MRS component_guaranteesD) 1);
 by (rtac Client_i_Bounded 1);
 by (auto_tac(claset(),
-	 simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
-			     client_export Collect_eq_extend_set RS sym]));
+	 simpset() addsimps [o_apply, lift_export extend_set_eq_Collect,
+			     client_export extend_set_eq_Collect]));
 qed "System_Bounded_ask";
 
 (*progress (2), step 4*)
@@ -479,7 +479,7 @@
 by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
 by (rtac INT_I 1);
 by (simp_tac (simpset() addsimps [o_apply]) 1);
-by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
+by (REPEAT (stac (lift_export extend_set_eq_Collect RS sym) 1));
 by (rtac (lift_export project_Ensures_D) 1);
 by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
 					   drop_prog_correct]) 1);
@@ -541,18 +541,17 @@
 by (Simp_tac 1);
 by (rtac INT_I 1);
 by (simp_tac (simpset() addsimps [o_apply]) 1);
-by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
+by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 1));
 by (rtac (client_export project_Ensures_D) 1);
 by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
 by (asm_full_simp_tac
     (simpset() addsimps [all_conj_distrib,
 			 Increasing_def, Stable_eq_stable, Join_stable,
-			 Collect_eq_extend_set RS sym]) 1);
+			 extend_set_eq_Collect]) 1);
 by (Clarify_tac 1);
 by (dtac G_stable_sysOfClient 1);
 by (auto_tac (claset(), 
-	      simpset() addsimps [o_apply,
-				client_export Collect_eq_extend_set RS sym]));
+     simpset() addsimps [o_apply, client_export extend_set_eq_Collect]));
 qed "sysOfClient_i_Progress";
 
 
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Client.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -46,10 +46,12 @@
 by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
 		       addSIs [stable_Int]) 3);
 by (constrains_tac 2);
+by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
 by Auto_tac;
 qed "ask_bounded_lemma";
 
-(*export version, with no mention of tok*)
+(*export version, with no mention of tok in the postcondition, but
+  unfortunately tok must be declared local.*)
 Goal "Client: UNIV guarantees[funPair ask tok] \
 \             Always {s. ALL elt : set (ask s). elt <= NbT}";
 by (rtac guaranteesI 1);
@@ -90,7 +92,6 @@
 qed "transient_lemma";
 
 
-
 Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
 \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
 \                     LeadsTo {s. k < rel s & rel s <= giv s & \
@@ -139,6 +140,7 @@
 			addDs [common_prefix_linear]) 1);
 qed "client_progress_lemma";
 
+(*Progress property: all tokens that are given will be released*)
 Goal "Client : \
 \      Increasing giv  guarantees[funPair rel ask]  \
 \      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
@@ -147,6 +149,28 @@
 by (blast_tac (claset() addIs [client_progress_lemma]) 1);
 qed "client_progress";
 
+Goal "Client : preserves extra";
+by (rewtac preserves_def);
+by Auto_tac;
+by (constrains_tac 1);
+by Auto_tac;
+qed "client_preserves_extra";
+
+Goal "bij client_map";
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [client_map_def, non_extra_def, bij_def, 
+				  inj_on_def, surj_def]));
+by (res_inst_tac 
+    [("x", "(|giv=?a, ask=?b, rel=?c, tok=?d, extra=?e|)")] exI 1);
+by (Force_tac 1);
+qed "bij_client_map";
+
+Goal "rename client_map Client : preserves snd";
+by (asm_simp_tac (simpset() addsimps [bij_client_map RS rename_preserves]) 1);
+by (asm_simp_tac (simpset() addsimps [client_map_def]) 1);
+by (rtac client_preserves_extra 1);
+qed "client_preserves_extra";
+
 
 (** Obsolete lemmas from first version of the Client **)
 
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Client.thy	Fri Feb 18 15:20:44 2000 +0100
@@ -6,7 +6,7 @@
 Distributed Resource Management System: the Client
 *)
 
-Client = Extend + 
+Client = Rename + 
 
 consts
   NbT :: nat       (*Maximum number of tokens*)
@@ -20,6 +20,10 @@
   rel :: tokbag list   (*output history: tokens released*)
   tok :: tokbag	       (*current token request*)
 
+record 'a state_u =
+  state +  
+  extra :: 'a          (*new variables*)
+
 
 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
 
@@ -27,7 +31,7 @@
   
   (** Release some tokens **)
   
-  rel_act :: "(state*state) set"
+  rel_act :: "('a state_u * 'a state_u) set"
     "rel_act == {(s,s').
 		  EX nrel. nrel = size (rel s) &
 		           s' = s (| rel := rel s @ [giv s!nrel] |) &
@@ -39,26 +43,27 @@
   (** Including s'=s suppresses fairness, allowing the non-trivial part
       of the action to be ignored **)
 
-  tok_act :: "(state*state) set"
-    "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}"
-
-  (*
-      "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
-  *)
-
+  tok_act :: "('a state_u * 'a state_u) set"
+     "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
   
-  ask_act :: "(state*state) set"
+  ask_act :: "('a state_u * 'a state_u) set"
     "ask_act == {(s,s'). s'=s |
 		         (s' = s (|ask := ask s @ [tok s]|))}"
 
-  Client :: state program
+  Client :: 'a state_u program
     "Client == mk_program ({s. tok s : atMost NbT &
 		               giv s = [] & ask s = [] & rel s = []},
 			   {rel_act, tok_act, ask_act})"
 
-  giv_meets_ask :: state set
-    "giv_meets_ask ==
-       {s. size (giv s) <= size (ask s) & 
-           (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
+  (*Maybe want a special theory section to declare such maps*)
+  non_extra :: 'a state_u => state
+    "non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+
+  (*Renaming map to put a Client into the standard form*)
+  client_map :: "'a state_u => state*'a"
+    "client_map == funPair non_extra extra"
+
+rules
+  NbT_pos  "0 < NbT"
 
 end
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -90,6 +90,16 @@
 
 (*** preserves ***)
 
+val prems = 
+Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
+by (blast_tac (claset() addIs prems) 1);
+qed "preservesI";
+
+Goalw [preserves_def, stable_def, constrains_def]
+     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'";
+by (Force_tac 1);
+qed "preserves_imp_eq";
+
 Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
 by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
 by (Blast_tac 1);
@@ -102,10 +112,14 @@
 
 AddIffs [Join_preserves, JN_preserves];
 
+Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
+by (Simp_tac 1);
+qed "funPair_apply";
+Addsimps [funPair_apply];
+
 Goal "preserves (funPair v w) = preserves v Int preserves w";
 by (auto_tac (claset(),
-	      simpset() addsimps [funPair_def, preserves_def, 
-				  stable_def, constrains_def]));
+	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
 by (Blast_tac 1);
 qed "preserves_funPair";
 
@@ -117,6 +131,17 @@
 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
 qed "funPair_o_distrib";
 
+
+Goal "fst o (funPair f g) = f";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "fst_o_funPair";
+
+Goal "snd o (funPair f g) = g";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "snd_o_funPair";
+Addsimps [fst_o_funPair, snd_o_funPair];
+
+
 Goal "preserves v <= preserves (w o v)";
 by (force_tac (claset(),
 	       simpset() addsimps [preserves_def, 
@@ -125,8 +150,7 @@
 
 Goal "preserves v <= stable {s. P (v s)}";
 by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, 
-				  stable_def, constrains_def]));
+	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
 by (rename_tac "s' s" 1);
 by (subgoal_tac "v s = v s'" 1);
 by (ALLGOALS Force_tac);
@@ -154,7 +178,7 @@
 by (Asm_simp_tac 2);
 by (dres_inst_tac [("P1", "split ?Q")]  
     (impOfSubs preserves_subset_stable) 1);
-by (auto_tac (claset(), simpset() addsimps [funPair_def]));
+by Auto_tac;
 qed "stable_localTo_stable2";
 
 Goal "[| F : stable {s. v s <= w s};  G : preserves v;       \
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -10,6 +10,10 @@
 
 (** These we prove OUTSIDE the locale. **)
 
+Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
+by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
+qed "insert_Id_image_Acts";
+
 (*Possibly easier than reasoning about "inv h"*)
 val [surj_h,prem] = 
 Goalw [good_map_def]
@@ -115,22 +119,25 @@
 qed "extend_set_strict_mono";
 AddIffs [extend_set_strict_mono];
 
-Goal "{s. P (f s)} = extend_set h {s. P s}";
+Goalw [extend_set_def] "extend_set h {} = {}";
 by Auto_tac;
-qed "Collect_eq_extend_set";
+qed "extend_set_empty";
+Addsimps [extend_set_empty];
+
+Goal "extend_set h {s. P s} = {s. P (f s)}";
+by Auto_tac;
+qed "extend_set_eq_Collect";
 
 Goal "extend_set h {x} = {s. f s = x}";
 by Auto_tac;
 qed "extend_set_sing";
 
-Goalw [extend_set_def]
-     "project_set h (extend_set h C) = C";
+Goalw [extend_set_def] "project_set h (extend_set h C) = C";
 by Auto_tac;
 qed "extend_set_inverse";
 Addsimps [extend_set_inverse];
 
-Goalw [extend_set_def]
-     "C <= extend_set h (project_set h C)";
+Goalw [extend_set_def] "C <= extend_set h (project_set h C)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [split_extended_all]));
 by (Blast_tac 1);
@@ -277,8 +284,7 @@
               simpset() addsimps [split_extended_all]) 1);
 qed "project_act_I";
 
-Goalw [project_act_def]
-    "UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
+Goalw [project_act_def] "project_act h Id = Id";
 by (Force_tac 1);
 qed "project_act_Id";
 
@@ -288,18 +294,7 @@
               simpset() addsimps [split_extended_all]) 1);
 qed "Domain_project_act";
 
-Addsimps [extend_act_Id, project_act_Id];
-
-Goal "(extend_act h act = Id) = (act = Id)";
-by Auto_tac;
-by (rewtac extend_act_def);
-by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
-qed "extend_act_Id_iff";
-
-Goal "Id : extend_act h `` Acts F";
-by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
-	      simpset() addsimps [image_iff]));
-qed "Id_mem_extend_act";
+Addsimps [extend_act_Id];
 
 
 (**** extend ****)
@@ -315,11 +310,10 @@
 qed "Init_project";
 
 Goal "Acts (extend h F) = (extend_act h `` Acts F)";
-by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
-	      simpset() addsimps [extend_def, image_iff]));
+by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
 qed "Acts_extend";
 
-Goal "Acts (project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
+Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
@@ -341,7 +335,6 @@
 by (Blast_tac 1);
 qed "project_set_Union";
 
-
 Goal "project h C (extend h F) = \
 \     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
 by (rtac program_equalityI 1);
@@ -378,7 +371,6 @@
 qed "extend_JN";
 Addsimps [extend_JN];
 
-
 (** These monotonicity results look natural but are UNUSED **)
 
 Goal "F <= G ==> extend h F <= extend h G";
@@ -460,7 +452,45 @@
 qed "extend_Always";
 
 
-(** Further lemmas **)
+(** Safety and "project" **)
+
+(** projection: monotonicity for safety **)
+
+Goal "D <= C ==> \
+\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
+qed "project_act_mono";
+
+Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
+by (dtac project_act_mono 1);
+by (Blast_tac 1);
+qed "project_constrains_mono";
+
+Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
+by (asm_full_simp_tac
+    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
+qed "project_stable_mono";
+
+Goalw [constrains_def]
+     "(project h C F : A co B)  =  \
+\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
+by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
+by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
+(*the <== direction*)
+by (rewtac project_act_def);
+by (force_tac (claset() addSDs [subsetD], simpset()) 1);
+qed "project_constrains";
+
+Goalw [stable_def]
+     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
+qed "project_stable";
+
+Goal "F : stable (extend_set h A) ==> project h C F : stable A";
+by (dtac (project_stable RS iffD2) 1);
+by (blast_tac (claset() addIs [project_stable_mono]) 1);
+qed "project_stable_I";
 
 Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
 by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
@@ -562,16 +592,84 @@
 by (etac leadsTo_imp_extend_leadsTo 2);
 by (dtac extend_leadsTo_slice 1);
 by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
-qed "extend_leadsto";
+qed "extend_leadsTo";
 
 Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =  \
 \     (F : A LeadsTo B)";
 by (simp_tac
     (simpset() addsimps [LeadsTo_def, reachable_extend_eq, 
-			 extend_leadsto, extend_set_Int_distrib RS sym]) 1);
+			 extend_leadsTo, extend_set_Int_distrib RS sym]) 1);
 qed "extend_LeadsTo";
 
 
+(*** preserves ***)
+
+Goal "G : preserves (v o f) ==> project h C G : preserves v";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, project_stable_I,
+				  extend_set_eq_Collect]));
+qed "project_preserves_I";
+
+(*to preserve f is to preserve the whole original state*)
+Goal "G : preserves f ==> project h C G : preserves id";
+by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
+qed "project_preserves_id_I";
+
+Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, extend_stable RS sym,
+				  extend_set_eq_Collect]));
+qed "extend_preserves";
+
+Goal "inj h ==> (extend h G : preserves g)";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
+				  stable_def, constrains_def, g_def]));
+qed "inj_extend_preserves";
+
+
+(*** Guarantees ***)
+
+Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
+by (rtac program_equalityI 1);
+by (asm_simp_tac
+    (simpset() addsimps [image_eq_UN, UN_Un, project_act_extend_act]) 2);
+by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
+qed "project_extend_Join";
+
+Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
+by (dres_inst_tac [("f", "project h UNIV")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
+qed "extend_Join_eq_extend_D";
+
+(** Strong precondition and postcondition; only useful when
+    the old and new state sets are in bijection **)
+
+Goal "F : X guarantees[v] Y ==> \
+\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
+by (rtac guaranteesI 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [project_preserves_I]
+			addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
+qed "guarantees_imp_extend_guarantees";
+
+Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
+\     ==> F : X guarantees[v] Y";
+by (auto_tac (claset(), simpset() addsimps [guar_def]));
+by (dres_inst_tac [("x", "extend h G")] spec 1);
+by (asm_full_simp_tac 
+    (simpset() delsimps [extend_Join] 
+           addsimps [extend_Join RS sym, extend_preserves,
+		     inj_extend RS inj_image_mem_iff]) 1);
+qed "extend_guarantees_imp_guarantees";
+
+Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
+\    (F : X guarantees[v] Y)";
+by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
+			       extend_guarantees_imp_guarantees]) 1);
+qed "extend_guarantees_eq";
+
+
 Close_locale "Extend";
 
 (*Close_locale should do this!
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Guar.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -120,7 +120,7 @@
 qed "guarantees_UN_left";
 
 Goalw [guar_def]
-    "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
+     "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
 by (Blast_tac 1);
 qed "guarantees_Un_left";
 
@@ -130,10 +130,15 @@
 qed "guarantees_INT_right";
 
 Goalw [guar_def]
-    "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
+     "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
 by (Blast_tac 1);
 qed "guarantees_Int_right";
 
+Goal "[| F : Z guarantees[v] X;  F : Z guarantees[v] Y |] \
+\    ==> F : Z guarantees[v] (X Int Y)";
+by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
+qed "guarantees_Int_right_I";
+
 Goal "(F : X guarantees[v] (INTER I Y)) = \
 \     (ALL i:I. F : X guarantees[v] (Y i))";
 by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -3,67 +3,87 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Arrays of processes.  Many results are instances of those in Extend & Project.
+Arrays of processes. 
 *)
 
+Addsimps [insert_map_def, delete_map_def];
 
-(*** Basic properties ***)
+Goal "delete_map i (insert_map i x f) = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "insert_map_inverse";
 
-(** lift_set and drop_set **)
+Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+by (exhaust_tac "d" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "insert_map_delete_map_eq";
+
+(*** Injectiveness proof ***)
 
-Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
-by Auto_tac;
-qed "lift_set_iff";
-AddIffs [lift_set_iff];
+Goal "(insert_map i x f) = (insert_map i y g) ==> x=y";
+by (dres_inst_tac [("x","i")] fun_cong 1);
+by (Full_simp_tac 1);
+qed "insert_map_inject1";
+
+Goal "(insert_map i x f) = (insert_map i y g) ==> f=g";
+by (dres_inst_tac [("f", "delete_map i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1);
+qed "insert_map_inject2";
 
-Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)";
+Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g";
+by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1);
+bind_thm ("insert_map_inject", result() RS conjE);
+AddSEs [insert_map_inject];
+
+(*The general case: we don't assume i=i'*)
+Goalw [lift_map_def]
+     "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \
+\     = (uu = uu' & insert_map i s f = insert_map i' s' f')"; 
 by Auto_tac;
-qed "Int_lift_set";
-
-Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)";
-by Auto_tac;
-qed "Un_lift_set";
-
-Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)";
-by Auto_tac;
-qed "Diff_lift_set";
-
-Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
-
-(** lift_act and drop_act **)
+qed "lift_map_eq_iff";
+AddIffs [lift_map_eq_iff];
 
-(*For compatibility with the original definition and perhaps simpler proofs*)
-Goalw [lift_act_def]
-    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
-by Auto_tac;
-by (rtac exI 1);
+Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s";
+by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1);
+qed "drop_map_lift_map_eq";
+
+Goalw [lift_map_def] "inj (lift_map i)";
+by (rtac injI 1);
 by Auto_tac;
-qed "lift_act_eq";
-AddIffs [lift_act_eq];
+qed "inj_lift_map";
 
-(** lift_prog and drop_prog **)
+(*** Surjectiveness proof ***)
 
-Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
-by Auto_tac;
-qed "Init_lift_prog";
-Addsimps [Init_lift_prog];
+Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s";
+by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1);
+qed "lift_map_drop_map_eq";
 
-Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
-by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
-qed "Acts_lift_prog";
-Addsimps [Acts_lift_prog];
+Goal "(drop_map i s) = (drop_map i s') ==> s=s'";
+by (dres_inst_tac [("f", "lift_map i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1);
+qed "drop_map_inject";
+AddSDs [drop_map_inject];
+
+Goal "surj (lift_map i)";
+by (rtac surjI 1);
+by (rtac lift_map_drop_map_eq 1);
+qed "surj_lift_map";
 
-Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)";
-by Auto_tac;
-qed "Init_drop_prog";
-Addsimps [Init_drop_prog];
+Goal "bij (lift_map i)";
+by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1);
+qed "bij_lift_map";
+AddIffs [bij_lift_map];
+
+AddIffs [bij_lift_map RS mem_rename_act_iff];
 
-Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
-by (auto_tac (claset() addIs [image_eqI], 
-	      simpset() addsimps [drop_prog_def]));
-qed "Acts_drop_prog";
-Addsimps [Acts_drop_prog];
-
+Goal "inv (lift_map i) = drop_map i";
+by (rtac inv_equality 1);
+by (rtac lift_map_drop_map_eq 2);
+by (rtac drop_map_lift_map_eq 1);
+qed "inv_lift_map_eq";
+Addsimps [inv_lift_map_eq];
 
 (*** sub ***)
 
@@ -72,374 +92,293 @@
 qed "sub_apply";
 Addsimps [sub_apply];
 
-Goal "lift_set i {s. P s} = {s. P (sub i s)}";
-by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
-qed "lift_set_sub";
-
-Goal "{s. P (s i)} = lift_set i {s. P s}";
-by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
-qed "Collect_eq_lift_set";
-
-Goal "sub i -`` A = lift_set i A";
-by (Force_tac 1);
-qed "sub_vimage";
-Addsimps [sub_vimage];
+Goal "lift_set i {s. P s} = {s. P (drop_map i s)}";
+by (rtac set_ext 1);
+by (asm_simp_tac (simpset() delsimps [image_Collect]
+			    addsimps [lift_set_def, rename_set_eq_Collect]) 1);
+qed "lift_set_eq_Collect";
 
-(*For tidying the result of "export"*)
-Goal "v o (%z. z i) = v o sub i";
-by (simp_tac (simpset() addsimps [sub_def]) 1);
-qed "fold_o_sub";
-
-
+Goalw [lift_set_def] "lift_set i {} = {}";
+by Auto_tac;
+qed "lift_set_empty";
+Addsimps [lift_set_empty];
 
-(*** lift_prog and the lattice operations ***)
-
-Goal "lift_prog i SKIP = SKIP";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [SKIP_def, lift_prog_def]));
-qed "lift_prog_SKIP";
+Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)";
+by (rtac (inj_lift_map RS inj_image_mem_iff) 1);
+qed "lift_set_iff";
+AddIffs [lift_set_iff];
 
-Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "lift_prog_Join";
-
-Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))";
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "lift_prog_JN";
-
-
-(*** Equivalence with "extend" version ***)
+Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
+by (asm_simp_tac (simpset() addsimps [lift_set_def, 
+				      mem_rename_set_iff, drop_map_def]) 1);
+qed "lift_set_iff";
+AddIffs [lift_set_iff];
 
-Goalw [lift_map_def] "good_map (lift_map i)";
-by (rtac good_mapI 1);
-by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1);
-by Auto_tac;
-by (dres_inst_tac [("f", "%f. f i")] arg_cong 1);
-by Auto_tac;
-qed "good_map_lift_map";
+Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
+by (etac image_mono 1);
+qed "lift_set_mono";
 
-fun lift_export0 th = 
-    good_map_lift_map RS export th 
-       |> simplify (simpset() addsimps [fold_o_sub]);
+Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B";
+by (asm_simp_tac (simpset() addsimps [image_Un]) 1);
+qed "lift_set_Un_distrib";
 
-Goal "fst (inv (lift_map i) g) = g i";
-by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
-by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
-qed "fst_inv_lift_map";
-Addsimps [fst_inv_lift_map];
+Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B";
+by (rtac (inj_lift_map RS image_set_diff) 1);
+qed "lift_set_Diff_distrib";
 
 
-Goal "lift_set i A = extend_set (lift_map i) A";
-by (auto_tac (claset(), 
-     simpset() addsimps [lift_export0 mem_extend_set_iff]));
-qed "lift_set_correct";
-
-Goalw [drop_set_def, project_set_def, lift_map_def]
-     "drop_set i A = project_set (lift_map i) A";
-by Auto_tac;
-by (rtac image_eqI 2);
-by (rtac exI 1);
-by (stac (refl RS fun_upd_idem) 1);
-by Auto_tac;
-qed "drop_set_correct";
-
-Goal "lift_act i = extend_act (lift_map i)";
-by (rtac ext 1);
-by Auto_tac;
-by (forward_tac [lift_export0 extend_act_D] 2);
-by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
-by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
-by (rtac bexI 1);
-by (auto_tac (claset() addSIs [exI], simpset()));
-qed "lift_act_correct";
+(*** the lattice operations ***)
 
-Goal "drop_act i = project_act (lift_map i)";
-by (rtac ext 1);
-by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
-by Auto_tac;
-by (REPEAT_FIRST (ares_tac [exI, conjI]));
-by Auto_tac;
-by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
-qed "drop_act_correct";
-
-Goal "lift_prog i = extend (lift_map i)";
-by (rtac (program_equalityI RS ext) 1);
-by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
-by (simp_tac (simpset() 
-	      addsimps [lift_export0 Acts_extend, 
-			lift_act_correct]) 1);
-qed "lift_prog_correct";
-
-Goal "drop_prog i C = project (lift_map i) C";
-by (rtac (program_equalityI RS ext) 1);
-by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
-by (simp_tac (simpset() 
-	      addsimps [Acts_project, drop_act_correct]) 1);
-qed "drop_prog_correct";
-
+Goalw [lift_def] "lift i SKIP = SKIP";
+by (Asm_simp_tac 1);
+qed "lift_SKIP";
+Addsimps [lift_SKIP];
 
-(** Injectivity of lift_set, lift_act, lift_prog **)
-
-Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
-by Auto_tac;
-qed "lift_set_inverse";
-Addsimps [lift_set_inverse];
-
-Goal "inj (lift_set i)";
-by (rtac inj_on_inverseI 1);
-by (rtac lift_set_inverse 1);
-qed "inj_lift_set";
-
-(*Because A and B could differ outside i, cannot generalize result to 
-   drop_set i (A Int B) = drop_set i A Int drop_set i B
-*)
-Goalw [lift_set_def, drop_set_def]
-     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
-by Auto_tac;
-qed "drop_set_Int_lift_set";
-
-Goalw [lift_set_def, drop_set_def]
-     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
-by Auto_tac;
-qed "drop_set_Int_lift_set2";
+Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G";
+by (Asm_simp_tac 1);
+qed "lift_Join";
+Addsimps [lift_Join];
 
-Goalw [drop_set_def]
-     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
-by Auto_tac;
-qed "drop_set_INT";
-
-Goal "lift_set i UNIV = UNIV";
-by (simp_tac (simpset() addsimps [lift_set_correct, 
-				  lift_export0 extend_set_UNIV_eq]) 1);
-qed "lift_set_UNIV_eq";
-Addsimps [lift_set_UNIV_eq];
-
-Goal "inj (lift_prog i)";
-by (simp_tac
-    (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
-qed "inj_lift_prog";
-
-
-(*** More Lemmas ***)
-
-Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
-by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
-				      lift_export0 extend_act_Image]) 1);
-qed "lift_act_Image";
-Addsimps [lift_act_Image];
-
-
+Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))";
+by (Asm_simp_tac 1);
+qed "lift_JN";
+Addsimps [lift_JN];
 
 (*** Safety: co, stable, invariant ***)
 
-(** Safety and lift_prog **)
-
-Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
-\     (F : A co B)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def]));
-by (Force_tac 1);
-qed "lift_prog_constrains";
-
-Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
-qed "lift_prog_stable";
-
-Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
-by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def, lift_prog_stable]));
-qed "lift_prog_invariant";
-
-Goal "[| lift_prog i F : A co B |] \
-\     ==> F : (drop_set i A) co (drop_set i B)";
-by (asm_full_simp_tac
-    (simpset() addsimps [drop_set_correct, lift_prog_correct, 
-			 lift_export0 extend_constrains_project_set]) 1);
-qed "lift_prog_constrains_drop_set";
+Goalw [lift_def, lift_set_def]
+     "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)";
+by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
+qed "lift_constrains";
 
-(*This one looks strange!  Proof probably is by case analysis on i=j.
-  If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
-  premise ensures A<=B.*)
-Goal "F i : A co B  \
-\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def]));
-by (REPEAT (Blast_tac 1));
-qed "constrains_imp_lift_prog_constrains";
-
+Goalw [lift_def, lift_set_def]
+     "(lift i F : stable (lift_set i A)) = (F : stable A)";
+by (asm_simp_tac (simpset() addsimps [rename_stable]) 1);
+qed "lift_stable";
 
-(** Safety and drop_prog **)
-
-Goal "(drop_prog i C F : A co B)  =  \
-\     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
-by (simp_tac
-    (simpset() addsimps [drop_prog_correct, lift_set_correct, 
-			 lift_export0 project_constrains]) 1);
-qed "drop_prog_constrains";
-
-Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
-by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
-qed "drop_prog_stable";
-
+Goalw [lift_def, lift_set_def]
+     "(lift i F : invariant (lift_set i A)) = (F : invariant A)";
+by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1);
+qed "lift_invariant";
 
-(*** Weak safety primitives: Co, Stable ***)
-
-(** Reachability **)
-
-Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
-by (simp_tac
-    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
-			 lift_export0 reachable_extend_eq]) 1);
-qed "reachable_lift_prog";
-
-Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
-\     (F : A Co B)";
-by (simp_tac
-    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
-			 lift_export0 extend_Constrains]) 1);
-qed "lift_prog_Constrains";
-
-Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
-by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
-qed "lift_prog_Stable";
+Goalw [lift_def, lift_set_def]
+     "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)";
+by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
+qed "lift_Constrains";
 
-Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B  \
-\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
-by (asm_full_simp_tac
-    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     lift_set_correct, lift_export0 project_Constrains_D]) 1);
-qed "drop_prog_Constrains_D";
-
-Goalw [Stable_def]
-     "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A  \
-\     ==> lift_prog i F Join G : Stable (lift_set i A)";
-by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
-qed "drop_prog_Stable_D";
+Goalw [lift_def, lift_set_def]
+     "(lift i F : Stable (lift_set i A)) = (F : Stable A)";
+by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1);
+qed "lift_Stable";
 
-Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A  \
-\     ==> lift_prog i F Join G : Always (lift_set i A)";
-by (asm_full_simp_tac
-    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     lift_set_correct, lift_export0 project_Always_D]) 1);
-qed "drop_prog_Always_D";
-
-Goalw [Increasing_def]
- "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \
-\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
-by Auto_tac;
-by (stac Collect_eq_lift_set 1);
-by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
-qed "project_Increasing_D";
-
+Goalw [lift_def, lift_set_def]
+     "(lift i F : Always (lift_set i A)) = (F : Always A)";
+by (asm_simp_tac (simpset() addsimps [rename_Always]) 1);
+qed "lift_Always";
 
 (*** Progress: transient, ensures ***)
 
-Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
-by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
-			  lift_export0 extend_transient]) 1);
-qed "lift_prog_transient";
+Goalw [lift_def, lift_set_def]
+     "(lift i F : transient (lift_set i A)) = (F : transient A)";
+by (asm_simp_tac (simpset() addsimps [rename_transient]) 1);
+qed "lift_transient";
+
+Goalw [lift_def, lift_set_def]
+     "(lift i F : (lift_set i A) ensures (lift_set i B)) = \
+\     (F : A ensures B)";
+by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1);
+qed "lift_ensures";
+
+Goalw [lift_def, lift_set_def]
+     "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \
+\     (F : A leadsTo B)";
+by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1);
+qed "lift_leadsTo";
 
-Goal "(lift_prog i F : transient (lift_set j A)) = \
-\     (i=j & F : transient A | A={})";
-by (case_tac "i=j" 1);
-by (auto_tac (claset(), simpset() addsimps [lift_prog_transient]));
-by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def]));
-by (Force_tac 1);
-qed "lift_prog_transient_eq_disj";
+Goalw [lift_def, lift_set_def]
+     "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =  \
+\     (F : A LeadsTo B)";
+by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1);
+qed "lift_LeadsTo";
+
+
+(** guarantees **)
+
+Goalw [lift_def]
+     "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
+\     (F : X guarantees[v] Y)";
+by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [o_def]) 1);
+qed "lift_lift_guarantees_eq";
+
+Goal "(lift i F : X guarantees[v] Y) = \
+\     (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
+\          (rename (drop_map i) `` Y))";
+by (asm_simp_tac 
+    (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
+			 lift_def]) 1);
+qed "lift_guarantees_eq_lift_inv";
 
 
-(*** guarantees properties ***)
+(*To preserve snd means that the second component is there just to allow
+  guarantees properties to be stated.  Converse fails, for lift i F can 
+  change function components other than i*)
+Goal "F : preserves snd ==> lift i F : preserves snd";
+by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1);
+by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
+by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1);
+qed "lift_preserves_snd_I";
+
+Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)";
+by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1);
+by (etac exI 1);
+bind_thm ("delete_map_eqE", result() RS exE);
+AddSEs [delete_map_eqE];
 
-Goal "lift_prog i F : preserves (v o sub j) = \
-\     (if i=j then F : preserves v else True)";
-by (simp_tac (simpset() addsimps [lift_prog_correct,
-				  lift_export0 extend_preserves]) 1);
+Goal "[| delete_map j g = delete_map j g';  i~=j |] ==> g i = g' i";
+by (Force_tac 1);
+qed "delete_map_neq_apply";
+
+(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
+
+Goal "(f o fst) -`` A = (f-``A) Times UNIV";
+by Auto_tac;
+qed "vimage_o_fst_eq";
+
+Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
+by Auto_tac;
+qed "vimage_sub_eq_lift_set";
+
+Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
+
+Goal "[| F : preserves snd;  i~=j |] \
+\     ==> lift j F : stable (lift_set i (A Times UNIV))";
 by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
-				  stable_def, constrains_def, lift_map_def]));
-qed "lift_prog_preserves_sub";
-
-Addsimps [lift_prog_preserves_sub];
+	      simpset() addsimps [lift_def, lift_set_def, 
+				  stable_def, constrains_def, 
+				  mem_rename_act_iff, mem_rename_set_iff]));
+by (auto_tac (claset() addSDs [preserves_imp_eq],
+	      simpset() addsimps [lift_map_def, drop_map_def]));
+by (dres_inst_tac [("x", "i")] fun_cong 1);
+by Auto_tac;
+qed "preserves_snd_lift_stable";
 
-Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
-by (asm_simp_tac
-    (simpset() addsimps [drop_prog_correct, fold_o_sub,
-			 lift_export0 project_preserves_I]) 1);
-qed "drop_prog_preserves_I";
+(*If i~=j then lift j F  does nothing to lift_set i, and the 
+  premise ensures A<=B.*)
+Goal "[| F i : (A Times UNIV) co (B Times UNIV);  \
+\        F j : preserves snd |]  \
+\  ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
+by (case_tac "i=j" 1);
+by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, 
+					   rename_constrains]) 1);
+by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1);
+by (assume_tac 1);
+by (etac (constrains_imp_subset RS lift_set_mono) 1);
+qed "constrains_imp_lift_constrains";
+
+(** Lemmas for the transient theorem **)
+
+Goal "(insert_map i t f)(i := s) = insert_map i s f";
+by (rtac ext 1);
+by Auto_tac;
+qed "insert_map_upd_same";
 
-(*The raw version*)
-val [xguary,drop_prog,lift_prog] =
-Goal "[| F : X guarantees[v] Y;  \
-\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X;  \
-\        !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
-\                G : preserves (v o sub i) |] \
-\             ==> lift_prog i F Join G : Y' |] \
-\     ==> lift_prog i F : X' guarantees[v o sub i] Y'";
-by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
-by (etac drop_prog_preserves_I 1);
-by (etac drop_prog 1);
+Goal "(insert_map j t f)(i := s) = \
+\     (if i=j then insert_map i s f \
+\      else if i<j then insert_map j t (f(i:=s)) \
+\      else insert_map j t (f(i-1:=s)))";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
+by (ALLGOALS arith_tac);
+qed "insert_map_upd";
+
+Goal "[| insert_map i s f = insert_map j t g;  i~=j |] \
+\     ==> EX g'. insert_map i s' f = insert_map j t g'";
+by (stac (insert_map_upd_same RS sym) 1);
+by (etac ssubst 1);
+by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1);
+by (Blast_tac 1);
+qed "insert_map_eq_diff";
+
+Goalw [lift_map_def]
+     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i~=j |] \
+\     ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))";
+by Auto_tac;
+by (blast_tac (claset() addDs [insert_map_eq_diff]) 1);
+qed "lift_map_eq_diff";
+
+Goal "F : preserves snd \
+\     ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
+\         (i=j & F : transient (A Times UNIV) | A={})";
+by (case_tac "i=j" 1);
+by (auto_tac (claset(), simpset() addsimps [lift_transient]));
+by (auto_tac (claset(),
+	      simpset() addsimps [lift_def, transient_def,
+				  Domain_rename_act]));
+by (dtac subsetD 1);
+by (Blast_tac 1);
 by Auto_tac;
-qed "drop_prog_guarantees_raw";
+ren "s f uu s' f' uu'" 1;
+by (subgoal_tac "f'=f & uu'=uu" 1);
+by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
+by Auto_tac;
+by (dtac sym 1);
+by (dtac subsetD 1);
+by (rtac ImageI 1);
+by (etac rename_actI 1);
+by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1);
+by (etac (lift_map_eq_diff RS exE) 1);
+by (assume_tac 1);
+by (dtac ComplD 1);
+by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1);
+qed "lift_transient_eq_disj";
 
-Goal "[| F : X guarantees[v] Y;  \
-\        projecting  C (lift_map i) F X' X;  \
-\        extending w C (lift_map i) F Y' Y; \
-\        preserves w <= preserves (v o sub i) |] \
-\     ==> lift_prog i F : X' guarantees[w] Y'";
-by (asm_simp_tac
-    (simpset() addsimps [lift_prog_correct, fold_o_sub,
-			 lift_export0 project_guarantees]) 1);
-qed "drop_prog_guarantees";
+(*USELESS??*)
+Goal "lift_map i `` (A Times UNIV) = \
+\     (UN s:A. UN f. {insert_map i s f}) Times UNIV";
+by (auto_tac (claset() addSIs [bexI, image_eqI],
+              simpset() addsimps [lift_map_def]));
+by (rtac (split RS sym) 1);
+qed "lift_map_image_Times";
+
+Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";
+by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
+qed "lift_preserves_eq";
+
+Goal "F : preserves snd \
+\     ==> lift i F : preserves (v o sub j o fst) = \
+\         (if i=j then F : preserves (v o fst) else True)";
+by (dtac (impOfSubs subset_preserves_o) 1);
+by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def,
+				       drop_map_lift_map_eq]) 1);
+by (asm_simp_tac (simpset() delcongs [if_weak_cong]
+			    addsimps [lift_map_def, 
+				      eq_commute, split_def, o_def]) 1);
+by Auto_tac;
+qed "lift_preserves_sub";
 
 
-(** Are these two useful?? **)
 
-(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
-  ensure that F has the form lift_prog i F for some F.*)
-Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
-by Auto_tac;
-by (stac Collect_eq_lift_set 1); 
-by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
-qed "image_lift_prog_Stable";
-
-Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
-by (simp_tac (simpset() addsimps [Increasing_def,
-				  inj_lift_prog RS image_INT]) 1);
-by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
-qed "image_lift_prog_Increasing";
-
-
-(*** guarantees corollaries ***)
+(*** guarantees corollaries [NOT USED]
 
 Goal "F : UNIV guarantees[v] increasing func \
-\   ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
+\   ==> lift i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
 by (dtac (lift_export0 extend_guar_increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_guar_increasing";
+by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
+qed "lift_guar_increasing";
 
 Goal "F : UNIV guarantees[v] Increasing func \
-\   ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
+\   ==> lift i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
 by (dtac (lift_export0 extend_guar_Increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_guar_Increasing";
+by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
+qed "lift_guar_Increasing";
 
 Goal "F : Always A guarantees[v] Always B \
-\ ==> lift_prog i F : \
+\ ==> lift i F : \
 \       Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
 by (asm_simp_tac
-    (simpset() addsimps [lift_set_correct, lift_prog_correct, 
+    (simpset() addsimps [lift_set_correct, lift_correct, 
 			 lift_export0 extend_guar_Always]) 1);
-qed "lift_prog_guar_Always";
-
-(*version for outside use*)
-fun lift_export th = 
-    good_map_lift_map RS export th 
-       |> simplify
-             (simpset() addsimps [fold_o_sub, 
-				  drop_set_correct RS sym, 
-				  lift_set_correct RS sym, 
-				  drop_prog_correct RS sym, 
-				  lift_prog_correct RS sym]);;
-
+qed "lift_guar_Always";
+***)
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Fri Feb 18 15:20:44 2000 +0100
@@ -6,35 +6,29 @@
 lift_prog, etc: replication of components
 *)
 
-Lift_prog = Project +
+Lift_prog = Rename +
 
 constdefs
 
-  lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)"
-    "lift_map i == %(s,f). f(i := s)"
-
-  lift_set :: "['a, 'b set] => ('a => 'b) set"
-    "lift_set i A == {f. f i : A}"
+  insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)"
+    "insert_map i z f k == if k<i then f k
+                           else if k=i then z
+                           else f(k-1)"
 
-  drop_set :: "['a, ('a=>'b) set] => 'b set"
-    "drop_set i A == (%f. f i) `` A"
-
-  lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
-    "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
+  delete_map :: "[nat, nat=>'b] => (nat=>'b)"
+    "delete_map i g k == if k<i then g k else g (Suc k)"
 
-  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
-    "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
+  lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c"
+    "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"
+
+  drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)"
+    "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
 
-  lift_prog :: "['a, 'b program] => ('a => 'b) program"
-    "lift_prog i F ==
-       mk_program (lift_set i (Init F),
-		   lift_act i `` Acts F)"
+  lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
+    "lift_set i A == lift_map i `` A"
 
-  (*Argument C allows weak safety laws to be projected*)
-  drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program"
-    "drop_prog i C F ==
-       mk_program (drop_set i (Init F),
-		   drop_act i `` Restrict C `` (Acts F))"
+  lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
+    "lift i == rename (lift_map i)"
 
   (*simplifies the expression of specifications*)
   constdefs
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -6,24 +6,20 @@
 Abstraction over replicated components (PLam)
 General products of programs (Pi operation)
 
-Probably some dead wood here!
+Some dead wood here!
 *)
 
-
-val image_eqI' = read_instantiate_sg (sign_of thy)
-                     [("x", "?ff(i := ?u)")] image_eqI;
-
 (*** Basic properties ***)
 
-Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
-by Auto_tac;
+Goal "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
 qed "Init_PLam";
 
-Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
-by (auto_tac (claset(),
-	      simpset() addsimps [PLam_def]));
+(*The "insert Id" is needed if I={}, since otherwise the RHS would be {} too*)
+Goal "Acts (PLam I F) = \
+\     insert Id (UN i:I. rename_act (lift_map i) `` Acts (F i))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def]) 1);
 qed "Acts_PLam";
-
 Addsimps [Init_PLam, Acts_PLam];
 
 Goal "PLam {} F = SKIP";
@@ -31,21 +27,20 @@
 qed "PLam_empty";
 
 Goal "(plam i: I. SKIP) = SKIP";
-by (simp_tac (simpset() addsimps [PLam_def,lift_prog_SKIP,JN_constant]) 1);
+by (simp_tac (simpset() addsimps [PLam_def,lift_SKIP,JN_constant]) 1);
 qed "PLam_SKIP";
 
 Addsimps [PLam_SKIP, PLam_empty];
 
-Goalw [PLam_def]
-    "PLam (insert i I) F = (lift_prog i (F i)) Join (PLam I F)";
+Goalw [PLam_def] "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)";
 by Auto_tac;
 qed "PLam_insert";
 
-Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
+Goal "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)";
 by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
 qed "PLam_component_iff";
 
-Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
+Goalw [PLam_def] "i : I ==> lift i (F i) <= (PLam I F)";
 (*blast_tac doesn't use HO unification*)
 by (fast_tac (claset() addIs [component_JN]) 1);
 qed "component_PLam";
@@ -53,240 +48,223 @@
 
 (** Safety & Progress **)
 
-Goal "i : I ==>  \
-\     (PLam I F : (lift_set i A) co (lift_set i B))  =  \
-\     (F i : A co B)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
-by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1, 
-			       constrains_imp_lift_prog_constrains]) 1);
+Goal "[| i : I;  ALL j. F j : preserves snd |] ==>  \
+\     (PLam I F : (lift_set i (A Times UNIV)) co \
+\                 (lift_set i (B Times UNIV)))  =  \
+\     (F i : (A Times UNIV) co (B Times UNIV))";
+by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
+				      Join_constrains]) 1);
+by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1);
 qed "PLam_constrains";
 
-Goal "i : I ==> (PLam I F : stable (lift_set i A)) = (F i : stable A)";
+Goal "[| i : I;  ALL j. F j : preserves snd |]  \
+\     ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
+\         (F i : stable (A Times UNIV))";
 by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
 qed "PLam_stable";
 
 Goal "i : I ==> \
-\   PLam I F : transient A = (EX i:I. lift_prog i (F i) : transient A)";
+\   PLam I F : transient A = (EX i:I. lift i (F i) : transient A)";
 by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
 qed "PLam_transient";
 
 Addsimps [PLam_constrains, PLam_stable, PLam_transient];
 
-Goal "[| i : I;  F i : A ensures B |] ==>  \
-\     PLam I F : (lift_set i A) ensures lift_set i B";
+(*This holds because the F j cannot change (lift_set i)*)
+Goal "[| i : I;  F i : (A Times UNIV) ensures (B Times UNIV);  \
+\        ALL j. F j : preserves snd |] ==>  \
+\     PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
 by (auto_tac (claset(), 
-	      simpset() addsimps [ensures_def, lift_prog_transient_eq_disj]));
+	      simpset() addsimps [ensures_def, lift_transient_eq_disj,
+				  lift_set_Un_distrib RS sym,
+				  lift_set_Diff_distrib RS sym,
+				  Times_Un_distrib1 RS sym,
+				  Times_Diff_distrib1 RS sym]));
 qed "PLam_ensures";
 
-Goal "[| i : I;  F i : (A-B) co (A Un B);  F i : transient (A-B) |] ==>  \
-\     PLam I F : (lift_set i A) leadsTo lift_set i B";
+Goal "[| i : I;  \
+\        F i : ((A Times UNIV) - (B Times UNIV)) co \
+\              ((A Times UNIV) Un (B Times UNIV));  \
+\        F i : transient ((A Times UNIV) - (B Times UNIV));  \
+\        ALL j. F j : preserves snd |] ==>  \
+\     PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
 by (rtac (PLam_ensures RS leadsTo_Basis) 1);
 by (rtac ensuresI 2);
 by (ALLGOALS assume_tac);
 qed "PLam_leadsTo_Basis";
 
-Goal "[| PLam I F : AA co BB;  i: I |] \
-\     ==> F i : (drop_set i AA) co (drop_set i BB)";
-by (rtac lift_prog_constrains_drop_set 1);
-(*rotate this assumption to be last*)
-by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
-qed "PLam_constrains_drop_set";
-
 
 (** invariant **)
 
-Goal "[| F i : invariant A;  i : I |] \
-\     ==> PLam I F : invariant (lift_set i A)";
+Goal "[| F i : invariant (A Times UNIV);  i : I;  \
+\        ALL j. F j : preserves snd |] \
+\     ==> PLam I F : invariant (lift_set i (A Times UNIV))";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def]));
 qed "invariant_imp_PLam_invariant";
 
-(*The f0 premise ensures that the product is well-defined.*)
-Goal "[| PLam I F : invariant (lift_set i A);  i : I;  \
-\        f0: Init (PLam I F) |] ==> F i : invariant A";
-by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def]));
-by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
-by Auto_tac;
-qed "PLam_invariant_imp_invariant";
+
+Goal "ALL j. F j : preserves snd \
+\     ==> (PLam I F : preserves (v o sub j o fst)) = \
+\         (if j: I then F j : preserves (v o fst) else True)";
+by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
+by (Blast_tac 1);
+qed "PLam_preserves";
+Addsimps [PLam_preserves];
+
 
-Goal "[| i : I;  f0: Init (PLam I F) |] \
-\     ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
-by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, 
-			       PLam_invariant_imp_invariant]) 1);
-qed "PLam_invariant";
+(**UNUSED
+    (*The f0 premise ensures that the product is well-defined.*)
+    Goal "[| PLam I F : invariant (lift_set i A);  i : I;  \
+    \        f0: Init (PLam I F) |] ==> F i : invariant A";
+    by (auto_tac (claset(),
+		  simpset() addsimps [invariant_def]));
+    by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
+    by Auto_tac;
+    qed "PLam_invariant_imp_invariant";
 
-(*The f0 premise isn't needed if F is a constant program because then
-  we get an initial state by replicating that of F*)
-Goal "i : I \
-\     ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
-by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def]));
-qed "const_PLam_invariant";
+    Goal "[| i : I;  f0: Init (PLam I F) |] \
+    \     ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
+    by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, 
+				   PLam_invariant_imp_invariant]) 1);
+    qed "PLam_invariant";
+
+    (*The f0 premise isn't needed if F is a constant program because then
+      we get an initial state by replicating that of F*)
+    Goal "i : I \
+    \     ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
+    by (auto_tac (claset(),
+		  simpset() addsimps [invariant_def]));
+    qed "const_PLam_invariant";
+**)
 
 
-(** Reachability **)
+(**UNUSED
+    (** Reachability **)
 
-Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
-by (etac reachable.induct 1);
-by (auto_tac (claset() addIs reachable.intrs, simpset()));
-qed "reachable_PLam";
+    Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
+    by (etac reachable.induct 1);
+    by (auto_tac (claset() addIs reachable.intrs, simpset()));
+    qed "reachable_PLam";
 
-(*Result to justify a re-organization of this file*)
-Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
-by Auto_tac;
-result();
+    (*Result to justify a re-organization of this file*)
+    Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
+    by Auto_tac;
+    result();
 
-Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
-by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
-qed "reachable_PLam_subset1";
+    Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
+    by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
+    qed "reachable_PLam_subset1";
 
-(*simplify using reachable_lift_prog??*)
-Goal "[| i ~: I;  A : reachable (F i) |]     \
-\  ==> ALL f. f : reachable (PLam I F)      \
-\             --> f(i:=A) : reachable (lift_prog i (F i) Join PLam I F)";
-by (etac reachable.induct 1);
-by (ALLGOALS Clarify_tac);
-by (etac reachable.induct 1);
-(*Init, Init case*)
-by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
-(*Init of F, action of PLam F case*)
-by (res_inst_tac [("act","act")] reachable.Acts 1);
-by (Force_tac 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset()) 1);
-(*induction over the 2nd "reachable" assumption*)
-by (eres_inst_tac [("xa","f")] reachable.induct 1);
-(*Init of PLam F, action of F case*)
-by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
-by (Force_tac 1);
-by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
-by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
-(*last case: an action of PLam I F*)
-by (res_inst_tac [("act","acta")] reachable.Acts 1);
-by (Force_tac 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset()) 1);
-qed_spec_mp "reachable_lift_Join_PLam";
-
-
-(*The index set must be finite: otherwise infinitely many copies of F can
-  perform actions, and PLam can never catch up in finite time.*)
-Goal "finite I \
-\     ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
-by (etac finite_induct 1);
-by (Simp_tac 1);
-by (force_tac (claset() addDs [reachable_lift_Join_PLam], 
-	       simpset() addsimps [PLam_insert]) 1);
-qed "reachable_PLam_subset2";
-
-Goal "finite I ==> \
-\     reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
-by (REPEAT_FIRST (ares_tac [equalityI,
-			    reachable_PLam_subset1, 
-			    reachable_PLam_subset2]));
-qed "reachable_PLam_eq";
+    (*simplify using reachable_lift??*)
+    Goal "[| i ~: I;  A : reachable (F i) |]     \
+    \  ==> ALL f. f : reachable (PLam I F)      \
+    \             --> f(i:=A) : reachable (lift i (F i) Join PLam I F)";
+    by (etac reachable.induct 1);
+    by (ALLGOALS Clarify_tac);
+    by (etac reachable.induct 1);
+    (*Init, Init case*)
+    by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
+    (*Init of F, action of PLam F case*)
+    by (res_inst_tac [("act","act")] reachable.Acts 1);
+    by (Force_tac 1);
+    by (assume_tac 1);
+    by (force_tac (claset() addIs [ext], simpset()) 1);
+    (*induction over the 2nd "reachable" assumption*)
+    by (eres_inst_tac [("xa","f")] reachable.induct 1);
+    (*Init of PLam F, action of F case*)
+    by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
+    by (Force_tac 1);
+    by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
+    by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
+    (*last case: an action of PLam I F*)
+    by (res_inst_tac [("act","acta")] reachable.Acts 1);
+    by (Force_tac 1);
+    by (assume_tac 1);
+    by (force_tac (claset() addIs [ext], simpset()) 1);
+    qed_spec_mp "reachable_lift_Join_PLam";
 
 
-(** Co **)
-
-Goal "[| F i : A Co B;  i: I;  finite I |]  \
-\     ==> PLam I F : (lift_set i A) Co (lift_set i B)";
-by (auto_tac
-    (claset(),
-     simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
-			 reachable_PLam_eq]));
-by (auto_tac (claset(), 
-              simpset() addsimps [constrains_def, PLam_def]));
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "Constrains_imp_PLam_Constrains";
+    (*The index set must be finite: otherwise infinitely many copies of F can
+      perform actions, and PLam can never catch up in finite time.*)
+    Goal "finite I \
+    \     ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
+    by (etac finite_induct 1);
+    by (Simp_tac 1);
+    by (force_tac (claset() addDs [reachable_lift_Join_PLam], 
+		   simpset() addsimps [PLam_insert]) 1);
+    qed "reachable_PLam_subset2";
 
-Goal "[| ALL j:I. f0 j : A j;   i: I |] \
-\     ==> drop_set i (INT j:I. lift_set j (A j)) = A i";
-by (force_tac (claset() addSIs [image_eqI'],
-	       simpset() addsimps [drop_set_def]) 1);
-qed "drop_set_INT_lift_set";
-
-(*Again, we need the f0 premise so that PLam I F has an initial state;
-  otherwise its Co-property is vacuous.*)
-Goal "[| PLam I F : (lift_set i A) Co (lift_set i B);  \
-\        i: I;  finite I;  f0: Init (PLam I F) |]  \
-\     ==> F i : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
-by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
-by (blast_tac (claset() addIs [reachable.Init]) 2);
-by (dtac PLam_constrains_drop_set 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [drop_set_Int_lift_set2,
-			 drop_set_INT_lift_set, reachable_PLam_eq]) 1);
-qed "PLam_Constrains_imp_Constrains";
+    Goal "finite I ==> \
+    \     reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
+    by (REPEAT_FIRST (ares_tac [equalityI,
+				reachable_PLam_subset1, 
+				reachable_PLam_subset2]));
+    qed "reachable_PLam_eq";
 
 
-Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
-\     ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =  \
-\         (F i : A Co B)";
-by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
-			       PLam_Constrains_imp_Constrains]) 1);
-qed "PLam_Constrains";
+    (** Co **)
 
-Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
-\     ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
-by (asm_simp_tac (simpset() delsimps [Init_PLam]
-			    addsimps [Stable_def, PLam_Constrains]) 1);
-qed "PLam_Stable";
+    Goal "[| F i : A Co B;  i: I;  finite I |]  \
+    \     ==> PLam I F : (lift_set i A) Co (lift_set i B)";
+    by (auto_tac
+	(claset(),
+	 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
+			     reachable_PLam_eq]));
+    by (auto_tac (claset(), 
+		  simpset() addsimps [constrains_def, PLam_def]));
+    by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+    qed "Constrains_imp_PLam_Constrains";
+
 
 
-(** const_PLam (no dependence on i) doesn't require the f0 premise **)
-
-Goal "[| (plam x:I. F) : (lift_set i A) Co (lift_set i B);  \
-\        i: I;  finite I |]  \
-\     ==> F : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
-by (dtac PLam_constrains_drop_set 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [drop_set_INT,
-			 drop_set_Int_lift_set2, Collect_conj_eq RS sym,
-			 reachable_PLam_eq]) 1);
-qed "const_PLam_Constrains_imp_Constrains";
+    Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
+    \     ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =  \
+    \         (F i : A Co B)";
+    by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
+				   PLam_Constrains_imp_Constrains]) 1);
+    qed "PLam_Constrains";
 
-Goal "[| i: I;  finite I |]  \
-\     ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
-\         (F : A Co B)";
-by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
-			       const_PLam_Constrains_imp_Constrains]) 1);
-qed "const_PLam_Constrains";
-
-Goal "[| i: I;  finite I |]  \
-\     ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
-by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
-qed "const_PLam_Stable";
-
-Goalw [Increasing_def]
-     "[| i: I;  finite I |]  \
-\     ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
-by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
-by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
-by (asm_full_simp_tac
-    (simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
-qed "const_PLam_Increasing";
+    Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
+    \     ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
+    by (asm_simp_tac (simpset() delsimps [Init_PLam]
+				addsimps [Stable_def, PLam_Constrains]) 1);
+    qed "PLam_Stable";
 
 
-(*** guarantees properties ***)
+    (** const_PLam (no dependence on i) doesn't require the f0 premise **)
+
+    Goal "[| i: I;  finite I |]  \
+    \     ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
+    \         (F : A Co B)";
+    by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
+				   const_PLam_Constrains_imp_Constrains]) 1);
+    qed "const_PLam_Constrains";
+
+    Goal "[| i: I;  finite I |]  \
+    \     ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
+    by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
+    qed "const_PLam_Stable";
 
-Goalw [PLam_def]
-    "[| lift_prog i (F i): X guarantees[v] Y;  i : I;  \
-\        ALL j:I. i~=j --> lift_prog j (F j) : preserves v |]  \
-\    ==> (PLam I F) : X guarantees[v] Y";
-by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
-qed "guarantees_PLam_I";
+    Goalw [Increasing_def]
+	 "[| i: I;  finite I |]  \
+    \     ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
+    by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
+    by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
+    by (asm_full_simp_tac
+	(simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
+    qed "const_PLam_Increasing";
+
 
-Goal "(PLam I F : preserves (v o sub j)) = \
-\     (if j: I then F j : preserves v else True)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, lift_prog_preserves_sub]) 1);
-by (Blast_tac 1);
-qed "PLam_preserves";
+    (*** guarantees properties ***)
 
-AddIffs [PLam_preserves];
+    Goalw [PLam_def]
+	"[| lift i (F i): X guarantees[v] Y;  i : I;  \
+    \        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \
+    \    ==> (PLam I F) : X guarantees[v] Y";
+    by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
+    qed "guarantees_PLam_I";
+**)
+
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Fri Feb 18 15:20:44 2000 +0100
@@ -11,11 +11,12 @@
 
 constdefs
 
-  PLam  :: ['a set, 'a => 'b program] => ('a => 'b) program
-    "PLam I F == JN i:I. lift_prog i (F i)"
+  PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
+            => ((nat=>'b) * 'c) program"
+    "PLam I F == JN i:I. lift i (F i)"
 
 syntax
-  "@PLam" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3plam _:_./ _)" 10)
+  "@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10)
 
 translations
   "plam x:A. B"   == "PLam A (%x. B)"
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Project.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -10,66 +10,14 @@
 
 Open_locale "Extend";
 
-(** projection: monotonicity for safety **)
-
-Goal "D <= C ==> \
-\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_mono";
-
-Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-by (dtac project_act_mono 1);
-by (Blast_tac 1);
-qed "project_constrains_mono";
-
-Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
-by (asm_full_simp_tac
-    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
-qed "project_stable_mono";
-
 Goal "F : A co B ==> project h C (extend h F) : A co B";
 by (auto_tac (claset(), 
       simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
 qed "project_extend_constrains_I";
 
-Goal "UNIV <= project_set h C \
-\     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
-by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
-			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
-by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
-qed "project_extend_Join";
-
-Goal "UNIV <= project_set h C \
-\     ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
-by (dres_inst_tac [("f", "project h C")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
-qed "extend_Join_eq_extend_D";
-
 
 (** Safety **)
 
-Goalw [constrains_def]
-     "(project h C F : A co B)  =  \
-\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
-by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
-by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
-(*the <== direction*)
-by (rewtac project_act_def);
-by (force_tac (claset() addSDs [subsetD], simpset()) 1);
-qed "project_constrains";
-
-Goalw [stable_def]
-     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
-by (simp_tac (simpset() addsimps [project_constrains]) 1);
-qed "project_stable";
-
-Goal "F : stable (extend_set h A) ==> project h C F : stable A";
-by (dtac (project_stable RS iffD2) 1);
-by (blast_tac (claset() addIs [project_stable_mono]) 1);
-qed "project_stable_I";
-
 (*used below to prove Join_project_ensures*)
 Goal "[| G : stable C;  project h C G : A unless B |] \
 \     ==> G : (C Int extend_set h A) unless (extend_set h B)";
@@ -113,7 +61,7 @@
      "extend h F Join G : increasing (func o f) \
 \     ==> F Join project h C G : increasing func";
 by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
-					   Collect_eq_extend_set RS sym]) 1);
+					   extend_set_eq_Collect]) 1);
 qed "project_increasing_I";
 
 Goal "(F Join project h UNIV G : increasing func)  =  \
@@ -123,7 +71,7 @@
 by (asm_full_simp_tac 
     (simpset() addsimps [increasing_def, Join_project_stable]) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
+	      simpset() addsimps [Join_stable, extend_set_eq_Collect,
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
@@ -136,32 +84,6 @@
 qed "project_constrains_D";
 
 
-(*** preserves ***)
-
-Goal "G : preserves (v o f) ==> project h C G : preserves v";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, project_stable_I,
-				  Collect_eq_extend_set RS sym]));
-qed "project_preserves_I";
-
-(*to preserve f is to preserve the whole original state*)
-Goal "G : preserves f ==> project h C G : preserves id";
-by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
-qed "project_preserves_id_I";
-
-Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, extend_stable RS sym,
-				  Collect_eq_extend_set RS sym]));
-qed "extend_preserves";
-
-Goal "inj h ==> (extend h G : preserves g)";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
-				  stable_def, constrains_def, g_def]));
-qed "inj_extend_preserves";
-
-
 (*** "projecting" and union/intersection (no converses) ***)
 
 Goalw [projecting_def]
@@ -315,7 +237,7 @@
      "F Join project h (reachable (extend h F Join G)) G : Increasing func  \
 \     ==> extend h F Join G : Increasing (func o f)";
 by Auto_tac;
-by (stac Collect_eq_extend_set 1);
+by (stac (extend_set_eq_Collect RS sym) 1);
 by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
 qed "project_Increasing_D";
 
@@ -381,7 +303,7 @@
     "extend h F Join G : Increasing (func o f)  \
 \    ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
 by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
+by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect,
 				      project_Stable_I]) 1); 
 qed "project_Increasing_I";
 
@@ -400,7 +322,7 @@
    "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  = \
 \   (extend h F Join G : Increasing (func o f))";
 by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
-				      Collect_eq_extend_set RS sym]) 1);
+				      extend_set_eq_Collect]) 1);
 qed "project_Increasing";
 
 (** A lot of redundant theorems: all are proved to facilitate reasoning
@@ -662,38 +584,9 @@
 qed "project_Ensures_D";
 
 
-(*** GUARANTEES and EXTEND ***)
-
-(** Strong precondition and postcondition; doesn't seem very useful. **)
-
-Goal "F : X guarantees[v] Y ==> \
-\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
-by (rtac guaranteesI 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [project_preserves_I]
-			addDs [project_set_UNIV RS equalityD2 RS 
-			       extend_Join_eq_extend_D, 
-			       guaranteesD]) 1);
-qed "guarantees_imp_extend_guarantees";
+(*** Guarantees ***)
 
-Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
-\     ==> F : X guarantees[v] Y";
-by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] spec 1);
-by (asm_full_simp_tac 
-    (simpset() delsimps [extend_Join] 
-           addsimps [extend_Join RS sym, extend_preserves,
-		     inj_extend RS inj_image_mem_iff]) 1);
-qed "extend_guarantees_imp_guarantees";
-
-Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
-\    (F : X guarantees[v] Y)";
-by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
-			       extend_guarantees_imp_guarantees]) 1);
-qed "extend_guarantees_eq";
-
-
-(*Weak precondition and postcondition; this is the good one!
+(*Weak precondition and postcondition
   Not clear that it has a converse [or that we want one!]*)
 
 (*The raw version*)
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -28,7 +28,9 @@
 time_use_thy "Extend";
 time_use_thy "PPROD";
 time_use_thy "TimerArray";
+(**
 time_use_thy "Alloc";
+**)
 
 add_path "../Auth";	(*to find Public.thy*)
 use_thy"NSP_Bad";
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/TimerArray.ML
--- a/src/HOL/UNITY/TimerArray.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -9,26 +9,40 @@
 Addsimps [Timer_def RS def_prg_Init];
 program_defs_ref := [Timer_def];
 
-Addsimps [decr_def];
+Addsimps [count_def, decr_def];
 
 (*Demonstrates induction, but not used in the following proof*)
-Goal "Timer : UNIV leadsTo {0}";
-by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
+Goal "Timer : UNIV leadsTo {s. count s = 0}";
+by (res_inst_tac [("f", "count")] lessThan_induct 1);
 by (Simp_tac 1);
 by (exhaust_tac "m" 1);
-by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
+by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
 by (ensures_tac "decr" 1);
 qed "Timer_leadsTo_zero";
 
-Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
-by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
+Goal "Timer : preserves snd";
+by (rtac preservesI 1);
+by (constrains_tac 1);
+qed "Timer_preserves_snd";
+AddIffs [Timer_preserves_snd];
+
+
+Goal "finite I \
+\     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
+by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
     (finite_stable_completion RS leadsTo_weaken) 1);
 by Auto_tac;
+(*Safety property, already reduced to the single Timer case*)
 by (constrains_tac 2);
-by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
+(*Progress property for the array of Timers*)
+by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
 by (exhaust_tac "m" 1);
+(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
 by (auto_tac (claset() addIs [subset_imp_leadsTo], 
-	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
+	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
+				  lift_set_Un_distrib RS sym,
+				  Times_Un_distrib1 RS sym,
+				  Times_Diff_distrib1 RS sym]));
 by (rename_tac "n" 1);
 by (rtac PLam_leadsTo_Basis 1);
 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/TimerArray.thy
--- a/src/HOL/UNITY/TimerArray.thy	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.thy	Fri Feb 18 15:20:44 2000 +0100
@@ -8,11 +8,16 @@
 
 TimerArray = PPROD +
 
+types 'a state = "nat * 'a"   (*second component allows new variables*)
+
 constdefs
-  decr  :: "(nat*nat) set"
-    "decr == UN n. {(Suc n, n)}"
+  count  :: "'a state => nat"
+    "count s == fst s"
   
-  Timer :: nat program
+  decr  :: "('a state * 'a state) set"
+    "decr == UN n uu. {((Suc n, uu), (n,uu))}"
+  
+  Timer :: 'a state program
     "Timer == mk_program (UNIV, {decr})"
 
 end
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Union.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -168,7 +168,9 @@
 
 (*** Safety: co, stable, FP ***)
 
-(*Fails if I={} because it collapses to SKIP : A co B*)
+(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
+  alternative precondition is A<=B, but most proofs using this rule require
+  I to be nonempty for other reasons anyway.*)
 Goalw [constrains_def, JOIN_def]
     "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
 by (Simp_tac 1);
@@ -196,6 +198,7 @@
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "Join_constrains_weaken";
 
+(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
 Goal "[| ALL i:I. F i : A i co A' i;  i: I |] \
 \     ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)";
 by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
@@ -258,10 +261,10 @@
 by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
 qed "Join_transient_I2";
 
+(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
 Goal "i : I ==> \
 \     (JN i:I. F i) : A ensures B = \
-\     ((ALL i:I. F i : (A-B) co (A Un B)) & \
-\      (EX i:I. F i : A ensures B))";
+\     ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))";
 by (auto_tac (claset(),
 	      simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
 qed "JN_ensures";
diff -r f4029c34adef -r 9be357df93d4 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML	Fri Feb 18 15:20:44 2000 +0100
@@ -401,11 +401,12 @@
 
 
 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
-Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
-\                   ((A Int f-``(lessThan m)) Un B) |] \
+val prems = 
+Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
 \     ==> F : A leadsTo B";
 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
 by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs prems) 1);
 qed "lessThan_induct";
 
 Goal "[| ALL m:(greaterThan l).    \