# HG changeset patch
# User paulson
# Date 943977250 -3600
# Node ID e3237d8c18d682eca4fb89f1296b7e755bb03a4a
# Parent  23e2a2457c779340f7c59675d084d433fa30b7a5
working version with new theory ELT

diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -397,17 +397,21 @@
 
 (*Lemma (?).  A LOT of work just to lift "Client_Progress" to the array*)
 Goal "lift_prog i Client \
-\  : Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client)) \
-\    guarantees \
-\    (INT h. {s. h <=  (giv o sub i) s & \
-\                       h pfixGe (ask o sub i) s}  \
-\            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
+\        :  Increasing (giv o sub i) Int \
+\           ((funPair rel ask o sub i) LocalTo (lift_prog i Client)) \
+\          guarantees \
+\          (INT h. {s. h <=  (giv o sub i) s & \
+\                             h pfixGe (ask o sub i) s}  \
+\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
+\                  {s. tokens h <= (tokens o rel o sub i) s})";
 by (rtac (Client_Progress RS drop_prog_guarantees) 1);
-by (rtac (lift_export extending_LeadsTo RS extending_weaken RS
+by (rtac (lift_export extending_LeadsETo RS extending_weaken RS
 	  extending_INT) 2);
 by (rtac subset_refl 4);
-by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
-by (force_tac (claset(), simpset() addsimps [sub_def, lift_prog_correct]) 2);
+by (simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
+				  sub_def]) 3);
+by (force_tac (claset(), 
+	       simpset() addsimps [sub_def, lift_prog_correct]) 2);
 by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
 by (auto_tac (claset(), simpset() addsimps [o_def]));
 qed "Client_i_Progress";
@@ -415,15 +419,123 @@
 (*needed??*)
 Goalw [PLam_def]
      "(plam x:lessThan Nclients. Client) \
-\  : (INT i : lessThan Nclients. \
-\          Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client))) \
-\    guarantees \
-\    (INT i : lessThan Nclients. \
-\         INT h. {s. h <=  (giv o sub i) s & \
-\                       h pfixGe (ask o sub i) s}  \
-\            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
-br guarantees_JN_INT 1;
-br Client_i_Progress 1;
+\        : (INT i : lessThan Nclients. \
+\             Increasing (giv o sub i) Int \
+\             ((funPair rel ask o sub i) LocalTo (lift_prog i Client))) \
+\          guarantees \
+\          (INT i : lessThan Nclients. \
+\               INT h. {s. h <=  (giv o sub i) s & \
+\                             h pfixGe (ask o sub i) s}  \
+\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
+\                    {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac guarantees_JN_INT 1);
+by (rtac Client_i_Progress 1);
 qed "PLam_Client_Progress";
 
 (*progress (2), step 7*)
+
+
+
+       [| ALL i:lessThan Nclients.
+             G : (sub i o client) LocalTo
+                 extend sysOfClient (lift_prog i Client) |]
+       ==> G : client LocalTo
+               extend sysOfClient (plam i:lessThan Nclients. Client)
+
+   
+   
+   
+   [| ALL i: I.
+	 G : (sub i o client) LocalTo
+	     extend sysOfClient (lift_prog i Client) |]
+   ==> G : client LocalTo
+	   extend sysOfClient (plam x: I. Client)
+
+
+Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
+     "[| ALL i. G : (sub i o v) localTo[C] F |] ==> G : v localTo[C] F";
+by Auto_tac;
+by (case_tac "Restrict C x: Restrict C `` Acts F" 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+by (rtac ext 1);
+by (blast_tac (claset() addSDs [bspec]) 1);
+qed "all_sub_localTo";
+
+
+
+ G : (sub i o client) LocalTo extend sysOfClient (plam x: I. Client)
+
+
+xxxxxxxxxxxxxxxx;
+
+THIS PROOF requires an extra locality specification for Network:
+    Network : rel o sub i o client localTo[C] 
+                     extend sysOfClient (lift_prog i Client)
+and similarly for ask o sub i o client.
+
+
+
+Goalw [System_def]
+ "System : (INT i : lessThan Nclients. \
+\         INT h. {s. h <= (giv o sub i o client) s & \
+\                         h pfixGe (ask o sub i o client) s}  \
+\                LeadsTo[givenBy (funPair rel ask o sub i o client)] \
+\                  {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
+by (rtac (PLam_Client_Progress RS project_guarantees) 1);
+br extending_INT 2;
+by (rtac (client_export extending_LeadsETo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
+by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
+			      client_export projecting_Increasing,
+			      component_PLam,
+			      client_export projecting_LocalTo]) 1);
+auto();
+
+be INT_lower 2;
+
+br projecting_INT 1;
+br projecting_Int 1;
+
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
+			      client_export projecting_Increasing,
+			      component_PLam,
+			      client_export projecting_LocalTo]) 1);
+by (Clarify_tac 2);
+by (asm_simp_tac
+    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+			 LocalTo_def, Join_localTo,
+			 sysOfClient_in_client_localTo_xl_Client,
+			 sysOfAlloc_in_client_localTo_xl_Client 
+			  RS localTo_imp_o_localTo,
+			 self_localTo]) 2);
+by Auto_tac;
+
+
+
+OLD PROOF;
+by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
+by (rtac (guarantees_PLam_I RS project_guarantees) 1);
+by (rtac Client_i_Progress 1);
+by (Force_tac 1);
+by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
+by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int,
+			      client_export projecting_Increasing,
+			      component_PLam,
+			      client_export projecting_LocalTo]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+			 LocalTo_def, Join_localTo,
+			 sysOfClient_in_client_localTo_xl_Client,
+			 sysOfAlloc_in_client_localTo_xl_Client]) 2);
+by Auto_tac;
+
+
+
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy	Tue Nov 30 16:54:10 1999 +0100
@@ -10,7 +10,7 @@
   --but need invariants that values are non-negative
 *)
 
-Alloc = Follows + Project + PPROD +
+Alloc = Follows + PPROD +
 
 (*Duplicated from HOL/ex/NatSum.thy.
   Maybe type should be  [nat=>int, nat] => int**)
@@ -84,7 +84,7 @@
 	 Increasing giv
 	 guarantees
 	 (INT h. {s. h <= giv s & h pfixGe ask s}
-		 LeadsTo
+		 LeadsTo[givenBy (funPair rel ask)]
 		 {s. tokens h <= (tokens o rel) s})"
 
   client_spec :: clientState program set
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Client.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -89,7 +89,7 @@
 Goal "Cli_prg Join G   \
 \       : transient {s. size (giv s) = Suc k &  \
 \                       size (rel s) = k & ask s ! k <= giv s ! k}";
-by (res_inst_tac [("act", "rel_act")] transient_mem 1);
+by (res_inst_tac [("act", "rel_act")] transientI 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [Domain_def, Cli_prg_def]));
 qed "transient_lemma";
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -399,6 +399,11 @@
 by (Force_tac 1);
 qed "extend_constrains_project_set";
 
+Goal "extend h F : stable A ==> F : stable (project_set h A)";
+by (asm_full_simp_tac
+    (simpset() addsimps [stable_def, extend_constrains_project_set]) 1);
+qed "extend_stable_project_set";
+
 
 (*** Diff, needed for localTo ***)
 
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -49,7 +49,7 @@
 Addsimps [Init_lift_prog];
 
 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
-by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
+by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
 qed "Acts_lift_prog";
 Addsimps [Acts_lift_prog];
 
@@ -59,7 +59,7 @@
 Addsimps [Init_drop_prog];
 
 Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
-by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
+by (auto_tac (claset() addIs [image_eqI], 
 	      simpset() addsimps [drop_prog_def]));
 qed "Acts_drop_prog";
 Addsimps [Acts_drop_prog];
@@ -391,6 +391,18 @@
 
 (*** guarantees properties ***)
 
+(*The raw version*)
+val [xguary,drop_prog,lift_prog] =
+Goal "[| F : X guarantees Y;  \
+\        !!G. lift_prog i F Join G : X' ==> F Join proj G i G : X;  \
+\        !!G. [| F Join proj G i G : Y; lift_prog i F Join G : X' |] \
+\             ==> lift_prog i F Join G : Y' |] \
+\     ==> lift_prog i F : X' guarantees Y'";
+by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
+by (etac drop_prog 1);
+by (assume_tac 1);
+qed "drop_prog_guarantees_raw";
+
 Goal "[| F : X guarantees Y;  \
 \        projecting C (lift_map i) F X' X;  \
 \        extending  C (lift_map i) F X' Y' Y |] \
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Nov 30 16:54:10 1999 +0100
@@ -6,7 +6,7 @@
 lift_prog, etc: replication of components
 *)
 
-Lift_prog = Project +
+Lift_prog = ELT +
 
 constdefs
 
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Project.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -12,7 +12,8 @@
 
 (** projection: monotonicity for safety **)
 
-Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
+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";
 
@@ -589,7 +590,7 @@
 \        F Join project h C G : A ensures B |] \
 \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
 by (auto_tac (claset() addDs [extend_transient RS iffD2] 
-                       addIs [transient_strengthen, 
+                       addIs [transient_strengthen, project_set_I,
 			      project_unless RS unlessD, unlessI, 
 			      project_extend_constrains_I], 
 	      simpset() addsimps [ensures_def, Join_constrains,
@@ -608,7 +609,7 @@
 by (etac leadsTo_induct 1);
 by (asm_simp_tac (simpset() delsimps UN_simps
 		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
+by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L, 
 			       leadsTo_Trans]) 2);
 by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
 val lemma = result();
@@ -673,7 +674,7 @@
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
 by (etac project 1);
 by (assume_tac 1);
-qed "project_guarantees_lemma";
+qed "project_guarantees_raw";
 
 Goal "[| F : X guarantees Y;  \
 \        projecting C h F X' X;  extending C h F X' Y' Y |] \
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -424,7 +424,7 @@
 				    ensuresI] 1),
 	      (*now there are two subgoals: co & transient*)
 	      simp_tac (simpset() addsimps !program_defs_ref) 2,
-	      res_inst_tac [("act", sact)] transient_mem 2,
+	      res_inst_tac [("act", sact)] transientI 2,
                  (*simplify the command's domain*)
 	      simp_tac (simpset() addsimps [Domain_def]) 3,
 	      constrains_tac 1,
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:54:10 1999 +0100
@@ -8,10 +8,8 @@
 
 SubstAx = WFair + Constrains + 
 
-consts
-   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
+constdefs
+   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
+    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
 
-defs
-   LeadsTo_def
-    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
 end
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/TimerArray.ML
--- a/src/HOL/UNITY/TimerArray.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/TimerArray.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -33,6 +33,6 @@
 by (rtac PLam_leadsTo_Basis 1);
 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
 by (constrains_tac 1);
-by (res_inst_tac [("act", "decr")] transient_mem 1);
+by (res_inst_tac [("act", "decr")] transientI 1);
 by (auto_tac (claset(), simpset() addsimps [Timer_def]));
 qed "TimerArray_leadsTo_zero";
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Union.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -338,6 +338,11 @@
 by (Force_tac 1);
 qed "localTo_imp_o_localTo";
 
+Goal "G : v LocalTo F ==> G : (f o v) LocalTo F";
+by (asm_full_simp_tac
+    (simpset() addsimps [LocalTo_def, localTo_imp_o_localTo]) 1);
+qed "LocalTo_imp_o_LocalTo";
+
 (*NOT USED*)
 Goalw [LOCALTO_def, stable_def, constrains_def]
      "(%s. x) localTo[C] F = UNIV";
@@ -366,12 +371,17 @@
 				  Join_left_absorb]) 1);
 qed "self_Join_LocalTo";
 
+Goalw [LOCALTO_def]
+     "[| G : v localTo[C] F;  F<=F' |] ==> G : v localTo[C] F'";
+by (Force_tac 1);
+qed "localTo_imp_o_localTo";
+
 
 
 (*** Higher-level rules involving localTo and Join ***)
 
-Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo[C] F |]  \
-\     ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
+Goal "[| F : {s. P (v s)} co B;  G : v localTo[C] F |]  \
+\     ==> G : C Int {s. P (v s)} co B";
 by (ftac constrains_imp_subset 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
@@ -392,12 +402,11 @@
 by (Blast_tac 1);
 qed "localTo_pairfun";
 
-Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
+Goal "[| F : {s. P (v s) (w s)} co B;   \
 \        G : v localTo[C] F;       \
 \        G : w localTo[C] F |]               \
-\     ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
-		  ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")] 
+\     ==> G : C Int {s. P (v s) (w s)} co B";
+by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}")] 
     constrains_weaken 1);
 by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
 by Auto_tac;
diff -r 23e2a2457c77 -r e3237d8c18d6 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/WFair.ML	Tue Nov 30 16:54:10 1999 +0100
@@ -29,7 +29,16 @@
 Goalw [transient_def]
     "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
 by (Blast_tac 1);
-qed "transient_mem";
+qed "transientI";
+
+val major::prems = 
+Goalw [transient_def]
+    "[| F : transient A;  \
+\       !!act. [| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> P |] \
+\    ==> P";
+by (rtac (major RS CollectD RS bexE) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "transientE";
 
 Goalw [transient_def] "transient UNIV = {}";
 by Auto_tac;
@@ -53,27 +62,24 @@
 by (Blast_tac 1);
 qed "ensuresD";
 
-(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
 Goalw [ensures_def]
     "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
 qed "ensures_weaken_R";
 
-Goalw [ensures_def, constrains_def, transient_def]
-    "F : A ensures UNIV";
-by Auto_tac;
-qed "ensures_UNIV";
-
+(*The L-version (precondition strengthening) fails, but we have this*)
 Goalw [ensures_def]
-    "[| F : stable C; \
-\       F : (C Int (A - A')) co (A Un A'); \
-\       F : transient (C Int (A-A')) |]   \
-\   ==> F : (C Int A) ensures (C Int A')";
-by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
-				      Diff_Int_distrib RS sym,
-				      stable_constrains_Int]) 1);
+    "[| F : stable C;  F : A ensures B |]   \
+\   ==> F : (C Int A) ensures (C Int B)";
+by (auto_tac (claset(),
+	      simpset() addsimps [ensures_def,
+				  Int_Un_distrib RS sym,
+				  Diff_Int_distrib RS sym]));
+by (blast_tac (claset() addIs [transient_strengthen]) 2);
+by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
 qed "stable_ensures_Int";
 
+(*NEVER USED*)
 Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
 by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
@@ -96,11 +102,6 @@
     (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
 qed "transient_imp_leadsTo";
 
-Goal "F : A leadsTo UNIV";
-by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
-qed "leadsTo_UNIV";
-Addsimps [leadsTo_UNIV];
-
 (*Useful with cancellation, disjunction*)
 Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
@@ -164,6 +165,9 @@
 bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
 Addsimps [empty_leadsTo];
 
+bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo);
+Addsimps [leadsTo_UNIV];
+
 
 Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
 by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
@@ -210,22 +214,6 @@
                         addIs prems) 1);
 qed "leadsTo_UN_UN";
 
-
-(*Version with no index set*)
-val prems = goal thy
-   "(!! i. F : (A i) leadsTo (A' i)) \
-\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [leadsTo_UN_UN] 
-                        addIs prems) 1);
-qed "leadsTo_UN_UN_noindex";
-
-(*Version with no index set*)
-Goal "ALL i. F : (A i) leadsTo (A' i) \
-\   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
-qed "all_leadsTo_UN_UN";
-
-
 (*Binary union version*)
 Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
 \     ==> F : (A Un B) leadsTo (A' Un B')";