new rule PLam_ensures
authorpaulson
Fri Sep 17 10:31:38 1999 +0200 (1999-09-17)
changeset 7538357873391561
parent 7537 875754b599df
child 7539 680eca63b98e
new rule PLam_ensures
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/PPROD.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Fri Sep 10 18:40:06 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Sep 17 10:31:38 1999 +0200
     1.3 @@ -17,6 +17,14 @@
     1.4  
     1.5  
     1.6  
     1.7 +Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
     1.8 +by (induct_tac "n" 1);
     1.9 +by Auto_tac;
    1.10 +by (dres_inst_tac [("x","n")] bspec 1);
    1.11 +by Auto_tac;
    1.12 +by (arith_tac 1);
    1.13 +qed_spec_mp "sum_mono";
    1.14 +
    1.15  
    1.16  (*Generalized version allowing different clients*)
    1.17  Goal "[| Alloc : alloc_spec;  \
    1.18 @@ -59,6 +67,7 @@
    1.19  	      simpset() addsimps [sysOfAlloc_def]));
    1.20  qed "inv_sysOfAlloc_eq";
    1.21  
    1.22 +Addsimps [inv_sysOfAlloc_eq];
    1.23  
    1.24  (**SHOULD NOT BE NECESSARY: The various injections into the system
    1.25     state need to be treated symmetrically or done automatically*)
    1.26 @@ -202,15 +211,13 @@
    1.27  qed "System_Increasing_allocRel";
    1.28  
    1.29  
    1.30 -(*NEED TO PROVE something like this (maybe without premise)*)
    1.31 -Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
    1.32 -
    1.33  fun alloc_export th = good_map_sysOfAlloc RS export th;
    1.34  
    1.35  val extend_Alloc_guar_Increasing =
    1.36    alloc_export extend_guar_Increasing
    1.37 -  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
    1.38 +  |> simplify (simpset());
    1.39  
    1.40 +(*step 2*)
    1.41  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
    1.42  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
    1.43  by (res_inst_tac 
    1.44 @@ -218,72 +225,30 @@
    1.45      component_guaranteesD 1);
    1.46  by (rtac Alloc_component_System 3);
    1.47  by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
    1.48 -by (rtac project_guarantees 1);
    1.49 -by (rtac Alloc_Safety 1);
    1.50 +by (rtac (Alloc_Safety RS project_guarantees) 1);
    1.51  by Auto_tac;
    1.52 -by (rtac project_Increasing_I 1);
    1.53 +(*1: Increasing precondition*)
    1.54 +by (stac (alloc_export project_Increasing) 1);
    1.55 +by (force_tac
    1.56 +    (claset(),
    1.57 +     simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
    1.58 +(*2: Always postcondition*)
    1.59 +by (dtac (subset_refl RS alloc_export project_Always_D) 1);
    1.60 +by (asm_full_simp_tac
    1.61 +     (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
    1.62 +qed "System_sum_bounded";
    1.63  
    1.64 -by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 
    1.65 -     THEN
    1.66 -     full_simp_tac
    1.67 -     (simpset() addsimps [inv_sysOfAlloc_eq,
    1.68 -			  alloc_export Collect_eq_extend_set RS sym]) 2);
    1.69 +(*step 3*)
    1.70 +Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients \
    1.71 +\                  <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}";
    1.72 +by (rtac (System_sum_bounded RS Always_weaken) 1);
    1.73 +by Auto_tac;
    1.74 +br order_trans 1;
    1.75 +br sum_mono 1;
    1.76 +bd order_trans 2;
    1.77 +br add_le_mono 2;
    1.78 +br order_refl 2;
    1.79 +br sum_mono 2;
    1.80 +ba 3;
    1.81  by Auto_tac;
    1.82  
    1.83 -by (dtac bspec 1);
    1.84 -by (Blast_tac 1);
    1.85 -
    1.86 -
    1.87 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
    1.88 -FIRST STEP WAS
    1.89 -by (res_inst_tac 
    1.90 -    [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
    1.91 -\                                       Int Increasing (sub i o allocRel))")] 
    1.92 -    component_guaranteesD 1);
    1.93 -
    1.94 -
    1.95 -       [| i < Nclients;
    1.96 -          extend sysOfAlloc Alloc Join G
    1.97 -          : (sub i o allocRel) localTo Network &
    1.98 -          extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
    1.99 -       ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
   1.100 -
   1.101 -
   1.102 -       [| i < Nclients;
   1.103 -          H : (sub i o allocRel) localTo Network &
   1.104 -          H : Increasing (sub i o allocRel) |]
   1.105 -       ==> project sysOfAlloc H : Increasing (sub i o allocRel)
   1.106 -
   1.107 -Open_locale"Extend";
   1.108 -
   1.109 -Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
   1.110 -by (asm_full_simp_tac 
   1.111 -    (simpset() addsimps [localTo_def, 
   1.112 -			 project_extend_Join RS sym,
   1.113 -			 Diff_project_stable,
   1.114 -			 Collect_eq_extend_set RS sym]) 1);
   1.115 -by Auto_tac;
   1.116 -by (rtac Diff_project_stable 1);
   1.117 -PROBABLY FALSE;
   1.118 -
   1.119 -by (Clarify_tac 1);
   1.120 -by (dres_inst_tac [("x","z")] spec 1);
   1.121 -
   1.122 -by (rtac (alloc_export project_Always_D) 2);
   1.123 -
   1.124 -by (rtac (alloc_export extend_Always RS iffD2) 2);
   1.125 -
   1.126 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.127 -
   1.128 -by (rtac guaranteesI 1);
   1.129 -
   1.130 -by (res_inst_tac 
   1.131 -    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
   1.132 -    component_guaranteesD 1);;
   1.133 -
   1.134 -
   1.135 -by (rtac (Alloc_Safety RS component_guaranteesD) 1);
   1.136 -
   1.137 -
   1.138 -by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1);
   1.139 -by (rtac Alloc_Safety 1);
     2.1 --- a/src/HOL/UNITY/Extend.ML	Fri Sep 10 18:40:06 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Sep 17 10:31:38 1999 +0200
     2.3 @@ -330,29 +330,45 @@
     2.4  (** Safety and project **)
     2.5  
     2.6  Goalw [constrains_def]
     2.7 -     "(project C h F : A co B)  =  \
     2.8 -\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
     2.9 -by (auto_tac (claset() addSIs [project_act_I], simpset()));
    2.10 +     "(F Join project C h G : A co B)  =  \
    2.11 +\       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
    2.12 +\        F : A co B)";
    2.13 +by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
    2.14 +by (force_tac (claset() addIs [extend_act_D], simpset()) 1);
    2.15 +by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
    2.16 +(*the <== direction*)
    2.17 +by (ball_tac 1);
    2.18  by (rewtac project_act_def);
    2.19 +by Auto_tac;
    2.20  by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1);
    2.21 -(*the <== direction*)
    2.22  by (force_tac (claset() addSDs [subsetD], simpset()) 1);
    2.23 -qed "project_constrains";
    2.24 +qed "Join_project_constrains";
    2.25  
    2.26  (*The condition is required to prove the left-to-right direction;
    2.27 -  could weaken it to F : (C Int extend_set h A) co C*)
    2.28 +  could weaken it to G : (C Int extend_set h A) co C*)
    2.29  Goalw [stable_def]
    2.30 -     "F : stable C \
    2.31 -\     ==> (project C h F : stable A)  =  (F : stable (C Int extend_set h A))";
    2.32 -by (simp_tac (simpset() addsimps [project_constrains]) 1);
    2.33 +     "extend h F Join G : stable C \
    2.34 +\     ==> (F Join project C h G : stable A)  =  \
    2.35 +\         (extend h F Join G : stable (C Int extend_set h A) &  \
    2.36 +\          F : stable A)";
    2.37 +by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
    2.38  by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
    2.39 -qed "project_stable";
    2.40 +qed "Join_project_stable";
    2.41  
    2.42 -Goal "(project UNIV h F : increasing func)  =  \
    2.43 -\     (F : increasing (func o f))";
    2.44 -by (asm_simp_tac (simpset() addsimps [increasing_def, project_stable,
    2.45 -				      Collect_eq_extend_set RS sym]) 1);
    2.46 -qed "project_increasing";
    2.47 +Goal "(F Join project UNIV h G : increasing func)  =  \
    2.48 +\     (extend h F Join G : increasing (func o f))";
    2.49 +by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
    2.50 +by (auto_tac (claset(),
    2.51 +	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
    2.52 +				  extend_stable RS iffD1]));
    2.53 +
    2.54 +qed "Join_project_increasing";
    2.55 +
    2.56 +Goal "(project C h F : A co B)  =  \
    2.57 +\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
    2.58 +by (cut_inst_tac [("F", "SKIP")] Join_project_constrains 1);
    2.59 +by (asm_full_simp_tac (simpset() addsimps [extend_SKIP]) 1);
    2.60 +qed "project_constrains";
    2.61  
    2.62  
    2.63  (*** Diff, needed for localTo ***)
    2.64 @@ -462,40 +478,46 @@
    2.65  
    2.66  (** Reachability and project **)
    2.67  
    2.68 -Goal "[| reachable F <= C;  z : reachable F |] \
    2.69 -\     ==> f z : reachable (project C h F)";
    2.70 +Goal "[| reachable (extend h F Join G) <= C;  \
    2.71 +\        z : reachable (extend h F Join G) |] \
    2.72 +\     ==> f z : reachable (F Join project C h G)";
    2.73  by (etac reachable.induct 1);
    2.74 -by (force_tac (claset() addIs [reachable.Acts, project_act_I],
    2.75 +by (force_tac (claset() delrules [Id_in_Acts]
    2.76 +		        addIs [reachable.Acts, project_act_I, extend_act_D],
    2.77  	       simpset()) 2);
    2.78  by (force_tac (claset() addIs [reachable.Init, project_set_I],
    2.79  	       simpset()) 1);
    2.80  qed "reachable_imp_reachable_project";
    2.81  
    2.82  Goalw [Constrains_def]
    2.83 -     "[| reachable F <= C;  project C h F : A Co B |] \
    2.84 -\     ==> F : (extend_set h A) Co (extend_set h B)";
    2.85 -by (full_simp_tac (simpset() addsimps [project_constrains]) 1);
    2.86 +     "[| reachable (extend h F Join G) <= C;    \
    2.87 +\        F Join project C h G : A Co B |] \
    2.88 +\     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
    2.89 +by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
    2.90  by (Clarify_tac 1);
    2.91 -by (etac constrains_weaken_L 1);
    2.92 +by (etac constrains_weaken 1);
    2.93  by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
    2.94  qed "project_Constrains_D";
    2.95  
    2.96  Goalw [Stable_def]
    2.97 -     "[| reachable F <= C;  project C h F : Stable A |] \
    2.98 -\     ==> F : Stable (extend_set h A)";
    2.99 +     "[| reachable (extend h F Join G) <= C;  \
   2.100 +\        F Join project C h G : Stable A |]   \
   2.101 +\     ==> extend h F Join G : Stable (extend_set h A)";
   2.102  by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
   2.103  qed "project_Stable_D";
   2.104  
   2.105  Goalw [Always_def]
   2.106 -     "[| reachable F <= C;  project C h F : Always A |] \
   2.107 -\     ==> F : Always (extend_set h A)";
   2.108 +     "[| reachable (extend h F Join G) <= C;  \
   2.109 +\        F Join project C h G : Always A |]   \
   2.110 +\     ==> extend h F Join G : Always (extend_set h A)";
   2.111  by (force_tac (claset() addIs [reachable.Init, project_set_I],
   2.112  	       simpset() addsimps [project_Stable_D]) 1);
   2.113  qed "project_Always_D";
   2.114  
   2.115  Goalw [Increasing_def]
   2.116 -     "[| reachable F <= C;  project C h F : Increasing func |] \
   2.117 -\     ==> F : Increasing (func o f)";
   2.118 +     "[| reachable (extend h F Join G) <= C;  \
   2.119 +\        F Join project C h G : Increasing func |] \
   2.120 +\     ==> extend h F Join G : Increasing (func o f)";
   2.121  by Auto_tac;
   2.122  by (stac Collect_eq_extend_set 1);
   2.123  by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
   2.124 @@ -504,71 +526,71 @@
   2.125  
   2.126  (** Converse results for weak safety: benefits of the argument C *)
   2.127  
   2.128 -Goal "[| C <= reachable F; x : reachable (project C h F) |] \
   2.129 -\     ==> EX y. h(x,y) : reachable F";
   2.130 +Goal "[| C <= reachable(extend h F Join G);   \
   2.131 +\        x : reachable (F Join project C h G) |] \
   2.132 +\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
   2.133  by (etac reachable.induct 1);
   2.134 -by (ALLGOALS 
   2.135 -    (asm_full_simp_tac
   2.136 -     (simpset() addsimps [project_set_def, project_act_def])));
   2.137 -by (force_tac (claset() addIs [reachable.Acts],
   2.138 +by (ALLGOALS Asm_full_simp_tac);
   2.139 +(*SLOW: 6.7s*)
   2.140 +by (force_tac (claset() delrules [Id_in_Acts]
   2.141 +		        addIs [reachable.Acts, extend_act_D],
   2.142  	       simpset() addsimps [project_act_def]) 2);
   2.143  by (force_tac (claset() addIs [reachable.Init],
   2.144  	       simpset() addsimps [project_set_def]) 1);
   2.145  qed "reachable_project_imp_reachable";
   2.146  
   2.147  Goalw [Constrains_def]
   2.148 -     "[| C <= reachable F;  F : (extend_set h A) Co (extend_set h B) |] \
   2.149 -\     ==> project C h F : A Co B";
   2.150 -by (full_simp_tac (simpset() addsimps [project_constrains, 
   2.151 +     "[| C <= reachable (extend h F Join G);  \
   2.152 +\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   2.153 +\     ==> F Join project C h G : A Co B";
   2.154 +by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
   2.155  				       extend_set_Int_distrib]) 1);
   2.156  by (rtac conjI 1);
   2.157 -by (force_tac (claset() addSDs [constrains_imp_subset, 
   2.158 -				reachable_project_imp_reachable], 
   2.159 -	       simpset()) 2);
   2.160  by (etac constrains_weaken 1);
   2.161  by Auto_tac;
   2.162 +by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
   2.163 +(*Some generalization of constrains_weaken_L would be better, but what is it?*)
   2.164 +by (rewtac constrains_def);
   2.165 +by Auto_tac;
   2.166 +by (thin_tac "ALL act : Acts G. ?P act" 1);
   2.167 +by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
   2.168 +	       simpset()) 1);
   2.169  qed "project_Constrains_I";
   2.170  
   2.171  Goalw [Stable_def]
   2.172 -     "[| C <= reachable F;  F : Stable (extend_set h A) |] \
   2.173 -\     ==> project C h F : Stable A";
   2.174 +     "[| C <= reachable (extend h F Join G);  \
   2.175 +\        extend h F Join G : Stable (extend_set h A) |] \
   2.176 +\     ==> F Join project C h G : Stable A";
   2.177  by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
   2.178  qed "project_Stable_I";
   2.179  
   2.180  Goalw [Increasing_def]
   2.181 -     "[| C <= reachable F;  F : Increasing (func o f) |] \
   2.182 -\     ==> project C h F : Increasing func";
   2.183 +     "[| C <= reachable (extend h F Join G);  \
   2.184 +\        extend h F Join G : Increasing (func o f) |] \
   2.185 +\     ==> F Join project C h G : Increasing func";
   2.186  by Auto_tac;
   2.187  by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
   2.188  				      project_Stable_I]) 1); 
   2.189  qed "project_Increasing_I";
   2.190  
   2.191 -Goal "(project (reachable F) h F : A Co B)  =  \
   2.192 -\     (F : (extend_set h A) Co (extend_set h B))";
   2.193 +Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
   2.194 +\     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
   2.195  by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
   2.196  qed "project_Constrains";
   2.197  
   2.198  Goalw [Stable_def]
   2.199 -     "(project (reachable F) h F : Stable A)  =  \
   2.200 -\     (F : Stable (extend_set h A))";
   2.201 +     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
   2.202 +\     (extend h F Join G : Stable (extend_set h A))";
   2.203  by (rtac project_Constrains 1);
   2.204  qed "project_Stable";
   2.205  
   2.206 -Goal "(project (reachable F) h F : Increasing func)  =  \
   2.207 -\     (F : Increasing (func o f))";
   2.208 +Goal
   2.209 +   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
   2.210 +\   (extend h F Join G : Increasing (func o f))";
   2.211  by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
   2.212  				      Collect_eq_extend_set RS sym]) 1);
   2.213  qed "project_Increasing";
   2.214  
   2.215 -(**
   2.216 -    (*NOT useful in its own right, but a guarantees rule likes premises
   2.217 -      in this form*)
   2.218 -    Goal "F Join project C h G : A Co B    \
   2.219 -    \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
   2.220 -    by (asm_simp_tac
   2.221 -	(simpset() addsimps [project_extend_Join, project_Constrains_D]) 1);
   2.222 -    qed "extend_Join_Constrains";
   2.223 -**)
   2.224  
   2.225  (*** Progress: transient, ensures ***)
   2.226  
   2.227 @@ -714,16 +736,14 @@
   2.228  Goal "F : UNIV guarantees increasing func \
   2.229  \     ==> extend h F : UNIV guarantees increasing (func o f)";
   2.230  by (etac project_guarantees 1);
   2.231 -by (asm_simp_tac (simpset() addsimps [project_increasing RS sym]) 2);
   2.232 -by (stac (project_set_UNIV RS project_extend_Join) 2);
   2.233 -by Auto_tac;
   2.234 +by (ALLGOALS
   2.235 +    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
   2.236  qed "extend_guar_increasing";
   2.237  
   2.238  Goal "F : UNIV guarantees Increasing func \
   2.239  \     ==> extend h F : UNIV guarantees Increasing (func o f)";
   2.240  by (etac project_guarantees 1);
   2.241  by (rtac (subset_UNIV RS project_Increasing_D) 2);
   2.242 -by (stac (project_set_UNIV RS project_extend_Join) 2);
   2.243  by Auto_tac;
   2.244  qed "extend_guar_Increasing";
   2.245  
   2.246 @@ -733,9 +753,7 @@
   2.247  by (etac project_guarantees 1);
   2.248  (*the "increasing" guarantee*)
   2.249  by (asm_simp_tac
   2.250 -    (simpset() addsimps [project_increasing RS sym]) 2);
   2.251 -by (stac (project_set_UNIV RS project_extend_Join) 2);
   2.252 -by (assume_tac 2);
   2.253 +    (simpset() addsimps [Join_project_increasing RS sym]) 2);
   2.254  (*the "localTo" requirement*)
   2.255  by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   2.256  by (asm_simp_tac 
   2.257 @@ -747,9 +765,7 @@
   2.258  \                      guarantees Increasing (func o f)";
   2.259  by (etac project_guarantees 1);
   2.260  (*the "Increasing" guarantee*)
   2.261 -by (rtac (subset_UNIV RS project_Increasing_D) 2);
   2.262 -by (stac (project_set_UNIV RS project_extend_Join) 2);
   2.263 -by (assume_tac 2);
   2.264 +by (etac (subset_UNIV RS project_Increasing_D) 2);
   2.265  (*the "localTo" requirement*)
   2.266  by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   2.267  by (asm_simp_tac 
     3.1 --- a/src/HOL/UNITY/PPROD.ML	Fri Sep 10 18:40:06 1999 +0200
     3.2 +++ b/src/HOL/UNITY/PPROD.ML	Fri Sep 17 10:31:38 1999 +0200
     3.3 @@ -64,10 +64,17 @@
     3.4  
     3.5  Addsimps [PLam_constrains, PLam_stable, PLam_transient];
     3.6  
     3.7 +Goal "[| i : I;  F i : A ensures B |] ==>  \
     3.8 +\     PLam I F : (lift_set i A) ensures lift_set i B";
     3.9 +by (auto_tac (claset(), 
    3.10 +	      simpset() addsimps [ensures_def, lift_prog_transient_eq_disj]));
    3.11 +qed "PLam_ensures";
    3.12 +
    3.13  Goal "[| i : I;  F i : (A-B) co (A Un B);  F i : transient (A-B) |] ==>  \
    3.14  \     PLam I F : (lift_set i A) leadsTo lift_set i B";
    3.15 -by (rtac (ensuresI RS leadsTo_Basis) 1);
    3.16 -by (auto_tac (claset(), simpset() addsimps [lift_prog_transient_eq_disj]));
    3.17 +by (rtac (PLam_ensures RS leadsTo_Basis) 1);
    3.18 +by (rtac ensuresI 2);
    3.19 +by (ALLGOALS assume_tac);
    3.20  qed "PLam_leadsTo_Basis";
    3.21  
    3.22  Goal "[| PLam I F : AA co BB;  i: I |] \