src/HOL/UNITY/Alloc.ML

--- a/src/HOL/UNITY/Alloc.ML	Wed Jun 23 10:37:29 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Wed Jun 23 10:38:09 1999 +0200
@@ -7,6 +7,19 @@
 *)
 
 
+(*Generalized version allowing different clients*)
+Goal "[| Alloc : alloc_spec;  \
+\        Client : (lessThan Nclients) funcset client_spec;  \
+\        Network : network_spec |] \
+\     ==> (extend sysOfAlloc Alloc) \
+\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
+\         Join Network : system_spec";
+
+Goal "System : system_spec";
+
+
+
+
 Addsimps [sub_def];
 
 Goalw [sysOfAlloc_def] "inj sysOfAlloc";
@@ -46,11 +59,11 @@
 
 Goalw [Increasing_def]
      "[| i: I;  finite I |]  \
-\     ==> ((PPI x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
+\     ==> ((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 [PFUN_Stable]) 1);
-qed "PFUN_Increasing";
+by (asm_full_simp_tac (simpset() addsimps [const_PLam_Stable]) 1);
+qed "const_PLam_Increasing";
 
 
 (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
@@ -70,7 +83,7 @@
 
 (*****************PPROD.ML******************)
 
-(*????????????????????????????????????????????????????????????????????????*)
+(*???????????????*)
 Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  modular i Y |] \
 \     ==> lift_prog i F : X guar Y";
 by (rtac guaranteesI 1);
@@ -128,17 +141,19 @@
 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
 qed "drop_prog_Stable_D";
 
-(***????????????????
+(***?????????????
 Goal "i ~= j ==> lift_prog i `` UNIV <= stable {s. P (f (s j))}";
 by Auto_tac;
 by (stac (lift_set_sub2 RS sym) 1); 
 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
 qed "image_lift_prog_Stable";
-????????????????*)
+??????????????*)
 
 
 
-(****UNITY.ML?****)
+(****UNITY.ML?  BUT it's not clear that Idle is good for anything.
+     Could equally want to forbid actions that are subsets of Id 
+   OR can simple constraints on actions prevent this?****)
 Goalw [constrains_def, Idle_def] "F : Idle ==> (F : A co B) = (A<=B)";
 by (Blast_tac 1);
 qed "constrains_Idle_iff";
@@ -150,9 +165,10 @@
 Goalw [drop_act_def, lift_act_def]
      "i~=j ==> drop_act i (lift_act j act) <= Id";
 by Auto_tac;
+be subst 1;
+by (Asm_simp_tac 1);
 qed "neq_drop_act_lift_act";
 
-
 Goal "drop_prog i (JN j:I - {i}. lift_prog j F) : Idle";
 by (simp_tac (simpset() addsimps [Acts_JN,Idle_def]) 1);
 by Auto_tac;
@@ -179,8 +195,148 @@
 by (blast_tac (claset() addIs [stable_Idle]) 1);
 qed "Idle_imp_stable_lift_set";
 
+(*like neq_drop_act_lift_act but stronger premises and conclusion*)
+Goal "[| i~=j;  act ~= {} |] ==> drop_act i (lift_act j act) = Id";
+br equalityI 1;
+be neq_drop_act_lift_act 1;
+by (asm_simp_tac (simpset() addsimps [drop_act_def, lift_act_def]) 1);
+by Auto_tac;
+ren "s s'" 1;
+by (dres_inst_tac [("x", "f(i:=x,j:=s)")] spec 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x", "f(i:=x,j:=s')")] spec 1);
+by (Asm_full_simp_tac 1);
+by (swap_res_tac [ext] 1);
+by (Asm_simp_tac 1);
+qed "neq_drop_act_lift_act_eq";
+
+
+Goal "act ~= {} ==> drop_act i (lift_act j act) = (if i=j then act else Id)";
+by (asm_simp_tac (simpset() addsimps [neq_drop_act_lift_act_eq]) 1);
+qed "drop_act_lift_act_eq";
+
+
+(*first premise says that the system has an initial state*)
+Goalw [PLam_def]
+     "[| ALL j:I. f0 j : Init (F j);   \
+\        ALL j:I. {}  ~: Acts (F j);   i: I |] \
+\     ==> drop_prog i (plam j:I. F j) = F i";
+by (simp_tac (simpset() addsimps [Acts_JN, lift_prog_def, drop_prog_def]) 1);
+by (rtac program_equalityI 1);
+by (asm_simp_tac (simpset() addsimps [drop_set_INT_lift_set]) 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac
+    "drop_act i `` (UN i:I. lift_act i `` Acts (F i)) = Acts (F i)" 1);
+by (Asm_simp_tac 1);
+by Auto_tac;
+ren "act" 1;
+by (subgoal_tac "act ~= {}" 1);
+by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [drop_act_lift_act_eq]) 1);
+br image_eqI 1;
+br (lift_act_inverse RS sym) 1;
+by Auto_tac;
+qed "drop_prog_plam_eq";
+
 xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
 
+(**STILL trying to lift the guarantees propery from one client to a family.
+   first with a "localTo" precondition.  Then to look at the void (UNIV) 
+   precondition.**)
+
+(*CANNOT be proved because the premise tells us NOTHING AT ALL about
+  actions outside i [rather than telling us there aren't any]
+  MAY UNIVERSALLY QUANTIFY both premise and conclusion???**)
+Goal "F : stable (lift_set i A) ==> x = lift_prog i (drop_prog i x)";
+
+(*I.E TRY THIS*)
+Goal "{F. F = (plam j:UNIV. drop_prog j F)} Int (INT i. stable (lift_set i A)) \
+\     <= (INT i. lift_prog i `` stable A)";
+
+
+Goal "{F. F = (plam j:UNIV. drop_prog j F)} Int stable (lift_set i A) \
+\     <= lift_prog i `` stable A";
+by Auto_tac;
+fr image_eqI;
+be (drop_prog_stable_eq RS iffD2) 2;
+be ssubst 1;
+by (stac drop_prog_plam_eq 1);
+by Auto_tac;
+
+
+by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
+qed "image_lift_prog_Stable";
+
+
+Goal "{F. F = (plam i:UNIV. drop_prog i F)} Int stable {s. P (f (s i))} \
+\     <= lift_prog i `` stable {s. P (f s)}";
+by (stac (lift_set_sub2 RS sym) 1); 
+
+
+Goal "Cl : (f localTo F) guar Increasing f   ==> \
+\ lift_prog i Cl : (f o sub i) localTo (lift_prog i F)  \
+\                  guar Increasing (f o sub i)";
+by (dtac lift_prog_guarantees 1);
+by (etac guarantees_weaken 1);
+by (rtac image_lift_prog_Increasing 2);
+
+
+
+
+
+
+
+Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
+
+
+
+
+
+
+Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
+by (simp_tac (simpset() addsimps [localTo_def]) 1);
+by Auto_tac;
+by (dres_inst_tac [("x","z")] spec 1);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym,
+				      lift_prog_stable_eq]) 1);
+qed "image_lift_prog_?";
+
+Goal "{GX. EX G: UNIV. lift_prog i G component GX} = UNIV";
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lift_set_def]) 1);
+ren "GX" 1;
+by (res_inst_tac [("x", "mk_program((%f. f i)``(Init GX), drop_act i `` Acts GX)")] exI 1);
+by Auto_tac;
+
+
+
+
+(*quantified formula's too strong and yet too weak.
+  Close to what's needed, but maybe need further restrictions on X, Y*)
+Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
+\        ALL j: -{i}. drop_prog j `` X <= drop_prog j `` Y |] \
+\     ==> lift_prog i F : X guar Y";
+by (rtac guaranteesI 1);
+by (dtac guaranteesD 1);
+by (rtac image_eqI 1);
+by (rtac (drop_prog_lift_prog_Join RS sym) 1);
+by (assume_tac 1);
+by Auto_tac;
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
+by (subgoal_tac "ALL k. drop_prog k (lift_prog i F Join G) = drop_prog k x" 1);
+by (Clarify_tac 2);
+by (case_tac "k=i" 2);
+by (Blast_tac 2);
+
+by (dres_inst_tac [("f", "lift_prog i")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [singleton_drop_prog_inverse]) 1);
+
+by (dtac sym 1);
+by (Blast_tac 1);
+qed "drop_prog_guarantees";
+
 Goalw [guarantees_def]
     "[| F : (X Int A) guar (Y Int A);  \
 \       F : (X Int B) guar (Y Int B);  \
@@ -222,15 +378,6 @@
 result();
 
 
-
-
-
-
-????????????????????????????????????????????????????????????????;
-
-
-
-
 Goal "drop_prog i `` UNIV = UNIV";
 by Auto_tac;
 fr image_eqI;
@@ -239,62 +386,6 @@
 result();
 
 
-Goal "[| F : (drop_prog i `` XX) guar Y;    \
-\        ALL Z:XX. Z component (JN i:UNIV. JN G:UNIV. lift_prog i G) |] \
-\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
-by (rtac guaranteesI 1);
-by (dtac guaranteesD 1);
-by (ball_tac 1);
-by (full_simp_tac (simpset() addsimps [Join_component_iff]) 1);
-by (full_simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
-
-by (rtac image_eqI 2);
-by (assume_tac 3);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 2);
-
-by (rtac (drop_prog_lift_prog_Join RS sym) 1);
-by (assume_tac 1);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
-by (rtac image_eqI 1);
-by (assume_tac 2);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
-
-by (rtac guaranteesI 1);
-by (dtac guaranteesD 1);
-by (rtac image_eqI 1);
-by (rtac (drop_prog_lift_prog_Join RS sym) 1);
-by (assume_tac 1);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
-by (rtac image_eqI 1);
-by (assume_tac 2);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
-
-
-by (dtac sym 1);
-by (Blast_tac 1);
-
-
-by (rtac guaranteesI 1);
-by (dtac guaranteesD 1);
-by (rtac image_eqI 2);
-by (assume_tac 3);
-
-
-Goal "F : X guar Y \
-\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
-by (rtac guaranteesI 1);
-by (dtac guaranteesD 1);
-by (rtac image_eqI 2);
-by (assume_tac 3);
-
-by Auto_tac;
-by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
-qed "lift_prog_guarantees";
-
-
-
-
-
 Goal "x : reachable (drop_prog i F) ==> x : drop_set i (reachable F)";
 by (etac reachable.induct 1);
 by Auto_tac;
@@ -315,16 +406,6 @@
 by (etac reachable_imp_reachable_drop_prog 2);
 
 
-(*FAILS, so the X condition is too strong*)
-Goal "((f o sub i) localTo (lift_prog i F))  <= (UN F. {lift_prog i F})";
-by (simp_tac (simpset() addsimps [localTo_def]) 1);
-by Auto_tac;
-
-
-Goal "lift_prog i `` drop_prog i `` ((f o sub i) localTo (lift_prog i F)) \
-\     <= ((f o sub i) localTo (lift_prog i F))";
-by (simp_tac (simpset() addsimps [localTo_def]) 1);
-by Auto_tac;
 
 
 
@@ -439,29 +520,6 @@
 result();
 
 
-Goal "H : lift_prog i `` drop_prog i `` X";
-
-
-Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
-\        X <= lift_prog i `` drop_prog i `` X;  \
-\        Y <= lift_prog i `` drop_prog i `` Y |] \
-\     ==> lift_prog i F : X guar Y";
-by (rtac guaranteesI 1);
-by (set_mp_tac 1);
-by (ALLGOALS Clarify_tac);
-by (dtac guaranteesD 1);
-by (rtac image_eqI 1);
-by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
-by (assume_tac 1);
-by (ALLGOALS Clarify_tac);
-by (set_mp_tac 1);
-by (ALLGOALS Clarify_tac);
-by Auto_tac;
-by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
-by Auto_tac;
-qed "drop_prog_guarantees";
 
 
 
@@ -470,26 +528,6 @@
 
 
 
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!;
-(*Precondition is TOO STRONG*)
-Goal "Cl : UNIV guar Increasing f \
-\     ==>lift_prog i Cl : (lift_prog i `` UNIV) guar Increasing (f o sub i)";
-by (rtac drop_prog_guarantees 1);
-by (etac guarantees_weaken 1);
-by Auto_tac;
-by (rtac (impOfSubs image_lift_prog_Increasing) 2);
-by (rtac image_eqI 1);
-by (rtac (lift_prog_inverse RS sym) 1);
-by (rtac (impOfSubs image_lift_prog_Increasing) 1);
-by Auto_tac;
-fr imageI;
-
-by (stac (lift_set_sub2 RS sym) 1); 
-by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
-
-
-
-
 
 
 Goal "Cl : UNIV guar Increasing f \
@@ -567,29 +605,6 @@
 
 
 
-Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
-
-
-
-
-
-
-Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
-by (simp_tac (simpset() addsimps [localTo_def]) 1);
-by Auto_tac;
-by (dres_inst_tac [("x","z")] spec 1);
-by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym,
-				      lift_prog_stable_eq]) 1);
-qed "image_lift_prog_?";
-
-Goal "{GX. EX G: UNIV. lift_prog i G component GX} = UNIV";
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_set_def]) 1);
-ren "GX" 1;
-by (res_inst_tac [("x", "mk_program((%f. f i)``(Init GX), drop_act i `` Acts GX)")] exI 1);
-by Auto_tac;
 
 
 by (stac Acts_eq 1);
@@ -619,16 +634,33 @@
 by (dtac lift_prog_guarantees 1);
 by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
 back();
-by (dtac (lessThan_iff RS iffD2 RS PFUN_Increasing RS iffD2) 1);
+by (dtac (lessThan_iff RS iffD2 RS const_PLam_Increasing RS iffD2) 1);
 by Auto_tac;
 
 
-by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (PFUN_Increasing RS sym)]) 1);
+by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (const_PLam_Increasing RS sym)]) 1);
 
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
 
 
-Goal "System : system_spec";
+!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!;
+(*Precondition is TOO STRONG*)
+Goal "Cl : UNIV guar Increasing f \
+\     ==>lift_prog i Cl : (lift_prog i `` UNIV) guar Increasing (f o sub i)";
+by (rtac drop_prog_guarantees 1);
+by (etac guarantees_weaken 1);
+by Auto_tac;
+by (rtac (impOfSubs image_lift_prog_Increasing) 2);
+by (rtac image_eqI 1);
+by (rtac (lift_prog_inverse RS sym) 1);
+by (rtac (impOfSubs image_lift_prog_Increasing) 1);
+by Auto_tac;
+fr imageI;
+
+by (stac (lift_set_sub2 RS sym) 1); 
+by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
+
+
 
 by (full_simp_tac
     (simpset() addsimps [alloc_spec_def, alloc_safety_def, System_def]) 1);
@@ -636,6 +668,63 @@
 
 
 
+Goal "[| F : (drop_prog i `` XX) guar Y;    \
+\        ALL Z:XX. Z component (JN i:UNIV. JN G:UNIV. lift_prog i G) |] \
+\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
+by (rtac guaranteesI 1);
+by (dtac guaranteesD 1);
+by (ball_tac 1);
+by (full_simp_tac (simpset() addsimps [Join_component_iff]) 1);
+by (full_simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
+
+by (rtac image_eqI 2);
+by (assume_tac 3);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 2);
+
+by (rtac (drop_prog_lift_prog_Join RS sym) 1);
+by (assume_tac 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
+by (rtac image_eqI 1);
+by (assume_tac 2);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
+
+by (rtac guaranteesI 1);
+by (dtac guaranteesD 1);
+by (rtac image_eqI 1);
+by (rtac (drop_prog_lift_prog_Join RS sym) 1);
+by (assume_tac 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
+by (rtac image_eqI 1);
+by (assume_tac 2);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
+
+
+by (dtac sym 1);
+by (Blast_tac 1);
+
+
+by (rtac guaranteesI 1);
+by (dtac guaranteesD 1);
+by (rtac image_eqI 2);
+by (assume_tac 3);
+
+
+Goal "F : X guar Y \
+\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
+by (rtac guaranteesI 1);
+by (dtac guaranteesD 1);
+by (rtac image_eqI 2);
+by (assume_tac 3);
+
+by Auto_tac;
+by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
+qed "lift_prog_guarantees";
+
+
+
+
+
+
 
 
 (*partial system...*)
@@ -644,7 +733,7 @@
 
 (*partial system...*)
 Goal "[| Client : client_spec;  Network : network_spec |] \
-\     ==> (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
+\     ==> (extend sysOfClient (plam x: lessThan Nclients. Client)) \
 \         Join Network : system_spec";
 
 
@@ -652,7 +741,7 @@
 Goal "[| Alloc : alloc_spec;  Client : client_spec;  \
 \        Network : network_spec |] \
 \     ==> (extend sysOfAlloc Alloc) \
-\         Join (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
+\         Join (extend sysOfClient (plam x: lessThan Nclients. Client)) \
 \         Join Network : system_spec";
 by (full_simp_tac
     (simpset() addsimps [system_spec_def, system_safety_def]) 1);
@@ -676,11 +765,65 @@
 
 
 
-(*Generalized version allowing different clients*)
-Goal "[| Alloc : alloc_spec;  \
-\        Client : (lessThan Nclients) funcset client_spec;  \
-\        Network : network_spec |] \
-\     ==> (extend sysOfAlloc Alloc) \
-\         Join (extend sysOfClient (PPROD (lessThan Nclients) Client)) \
-\         Join Network : system_spec";
+Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
+\        X <= lift_prog i `` drop_prog i `` X;  \
+\        Y <= lift_prog i `` drop_prog i `` Y |] \
+\     ==> lift_prog i F : X guar Y";
+by (rtac guaranteesI 1);
+by (set_mp_tac 1);
+by (ALLGOALS Clarify_tac);
+by (dtac guaranteesD 1);
+by (rtac image_eqI 1);
+by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
+by (assume_tac 1);
+by (ALLGOALS Clarify_tac);
+by (set_mp_tac 1);
+by (ALLGOALS Clarify_tac);
+by Auto_tac;
+by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
+by Auto_tac;
+qed "drop_prog_guarantees";
+
+
+
+
+(*****SINGLETON LEMMAS: GOOD FOR ANYTHING??????***)
 
+(*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
+*)
+Goal "[| ALL j. j = i; f i = g i |] ==> f = g";
+br ext 1;
+by (dres_inst_tac [("x", "x")] spec 1);
+by Auto_tac;
+qed "singleton_ext";
+
+Goalw [lift_set_def, drop_set_def]
+     "ALL j. j = i ==> lift_set i (drop_set i A) = A";
+by (blast_tac (claset() addSDs [singleton_ext]) 1);
+qed "singleton_drop_set_inverse";
+
+Goal "ALL j. j = i ==> f(i:= g i) = g";
+by (dres_inst_tac [("x", "x")] spec 1);
+by Auto_tac;
+qed "singleton_update_eq";
+
+Goalw [lift_act_def, drop_act_def]
+     "ALL j. j = i ==> lift_act i (drop_act i act) = act";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [singleton_update_eq]) 1);
+bd singleton_ext 1;
+ba 1;
+by (auto_tac (claset() addSIs [exI, image_eqI], 
+	      simpset() addsimps [singleton_update_eq]));
+qed "singleton_drop_act_inverse";
+
+Goal "ALL j. j = i ==> lift_prog i (drop_prog i F) = F";
+by (rtac program_equalityI 1);
+by (asm_simp_tac (simpset() addsimps [singleton_drop_set_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [image_compose RS sym, o_def,
+				      singleton_drop_act_inverse]) 1);
+qed "singleton_drop_prog_inverse";
+