new rule PLam_ensures

--- a/src/HOL/UNITY/Alloc.ML	Fri Sep 10 18:40:06 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Fri Sep 17 10:31:38 1999 +0200
@@ -17,6 +17,14 @@
 
 
 
+Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (dres_inst_tac [("x","n")] bspec 1);
+by Auto_tac;
+by (arith_tac 1);
+qed_spec_mp "sum_mono";
+
 
 (*Generalized version allowing different clients*)
 Goal "[| Alloc : alloc_spec;  \
@@ -59,6 +67,7 @@
 	      simpset() addsimps [sysOfAlloc_def]));
 qed "inv_sysOfAlloc_eq";
 
+Addsimps [inv_sysOfAlloc_eq];
 
 (**SHOULD NOT BE NECESSARY: The various injections into the system
    state need to be treated symmetrically or done automatically*)
@@ -202,15 +211,13 @@
 qed "System_Increasing_allocRel";
 
 
-(*NEED TO PROVE something like this (maybe without premise)*)
-Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
-
 fun alloc_export th = good_map_sysOfAlloc RS export th;
 
 val extend_Alloc_guar_Increasing =
   alloc_export extend_guar_Increasing
-  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
+  |> simplify (simpset());
 
+(*step 2*)
 Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
 \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
 by (res_inst_tac 
@@ -218,72 +225,30 @@
     component_guaranteesD 1);
 by (rtac Alloc_component_System 3);
 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
-by (rtac project_guarantees 1);
-by (rtac Alloc_Safety 1);
+by (rtac (Alloc_Safety RS project_guarantees) 1);
 by Auto_tac;
-by (rtac project_Increasing_I 1);
+(*1: Increasing precondition*)
+by (stac (alloc_export project_Increasing) 1);
+by (force_tac
+    (claset(),
+     simpset() addsimps [o_def, alloc_export project_Increasing]) 1);
+(*2: Always postcondition*)
+by (dtac (subset_refl RS alloc_export project_Always_D) 1);
+by (asm_full_simp_tac
+     (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
+qed "System_sum_bounded";
 
-by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 
-     THEN
-     full_simp_tac
-     (simpset() addsimps [inv_sysOfAlloc_eq,
-			  alloc_export Collect_eq_extend_set RS sym]) 2);
+(*step 3*)
+Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients \
+\                  <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}";
+by (rtac (System_sum_bounded RS Always_weaken) 1);
+by Auto_tac;
+br order_trans 1;
+br sum_mono 1;
+bd order_trans 2;
+br add_le_mono 2;
+br order_refl 2;
+br sum_mono 2;
+ba 3;
 by Auto_tac;
 
-by (dtac bspec 1);
-by (Blast_tac 1);
-
-
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
-FIRST STEP WAS
-by (res_inst_tac 
-    [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
-\                                       Int Increasing (sub i o allocRel))")] 
-    component_guaranteesD 1);
-
-
-       [| i < Nclients;
-          extend sysOfAlloc Alloc Join G
-          : (sub i o allocRel) localTo Network &
-          extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
-       ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
-
-
-       [| i < Nclients;
-          H : (sub i o allocRel) localTo Network &
-          H : Increasing (sub i o allocRel) |]
-       ==> project sysOfAlloc H : Increasing (sub i o allocRel)
-
-Open_locale"Extend";
-
-Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
-by (asm_full_simp_tac 
-    (simpset() addsimps [localTo_def, 
-			 project_extend_Join RS sym,
-			 Diff_project_stable,
-			 Collect_eq_extend_set RS sym]) 1);
-by Auto_tac;
-by (rtac Diff_project_stable 1);
-PROBABLY FALSE;
-
-by (Clarify_tac 1);
-by (dres_inst_tac [("x","z")] spec 1);
-
-by (rtac (alloc_export project_Always_D) 2);
-
-by (rtac (alloc_export extend_Always RS iffD2) 2);
-
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
-
-by (rtac guaranteesI 1);
-
-by (res_inst_tac 
-    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
-    component_guaranteesD 1);;
-
-
-by (rtac (Alloc_Safety RS component_guaranteesD) 1);
-
-
-by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1);
-by (rtac Alloc_Safety 1);

--- a/src/HOL/UNITY/Extend.ML	Fri Sep 10 18:40:06 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Sep 17 10:31:38 1999 +0200
@@ -330,29 +330,45 @@
 (** Safety and project **)
 
 Goalw [constrains_def]
-     "(project C h 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()));
+     "(F Join project C h G : A co B)  =  \
+\       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
+\        F : A co B)";
+by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
+by (force_tac (claset() addIs [extend_act_D], simpset()) 1);
+by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
+(*the <== direction*)
+by (ball_tac 1);
 by (rewtac project_act_def);
+by Auto_tac;
 by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1);
-(*the <== direction*)
 by (force_tac (claset() addSDs [subsetD], simpset()) 1);
-qed "project_constrains";
+qed "Join_project_constrains";
 
 (*The condition is required to prove the left-to-right direction;
-  could weaken it to F : (C Int extend_set h A) co C*)
+  could weaken it to G : (C Int extend_set h A) co C*)
 Goalw [stable_def]
-     "F : stable C \
-\     ==> (project C h F : stable A)  =  (F : stable (C Int extend_set h A))";
-by (simp_tac (simpset() addsimps [project_constrains]) 1);
+     "extend h F Join G : stable C \
+\     ==> (F Join project C h G : stable A)  =  \
+\         (extend h F Join G : stable (C Int extend_set h A) &  \
+\          F : stable A)";
+by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
-qed "project_stable";
+qed "Join_project_stable";
 
-Goal "(project UNIV h F : increasing func)  =  \
-\     (F : increasing (func o f))";
-by (asm_simp_tac (simpset() addsimps [increasing_def, project_stable,
-				      Collect_eq_extend_set RS sym]) 1);
-qed "project_increasing";
+Goal "(F Join project UNIV h G : increasing func)  =  \
+\     (extend h F Join G : increasing (func o f))";
+by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
+				  extend_stable RS iffD1]));
+
+qed "Join_project_increasing";
+
+Goal "(project C h F : A co B)  =  \
+\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
+by (cut_inst_tac [("F", "SKIP")] Join_project_constrains 1);
+by (asm_full_simp_tac (simpset() addsimps [extend_SKIP]) 1);
+qed "project_constrains";
 
 
 (*** Diff, needed for localTo ***)
@@ -462,40 +478,46 @@
 
 (** Reachability and project **)
 
-Goal "[| reachable F <= C;  z : reachable F |] \
-\     ==> f z : reachable (project C h F)";
+Goal "[| reachable (extend h F Join G) <= C;  \
+\        z : reachable (extend h F Join G) |] \
+\     ==> f z : reachable (F Join project C h G)";
 by (etac reachable.induct 1);
-by (force_tac (claset() addIs [reachable.Acts, project_act_I],
+by (force_tac (claset() delrules [Id_in_Acts]
+		        addIs [reachable.Acts, project_act_I, extend_act_D],
 	       simpset()) 2);
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
 	       simpset()) 1);
 qed "reachable_imp_reachable_project";
 
 Goalw [Constrains_def]
-     "[| reachable F <= C;  project C h F : A Co B |] \
-\     ==> F : (extend_set h A) Co (extend_set h B)";
-by (full_simp_tac (simpset() addsimps [project_constrains]) 1);
+     "[| reachable (extend h F Join G) <= C;    \
+\        F Join project C h G : A Co B |] \
+\     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
+by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
-by (etac constrains_weaken_L 1);
+by (etac constrains_weaken 1);
 by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
 qed "project_Constrains_D";
 
 Goalw [Stable_def]
-     "[| reachable F <= C;  project C h F : Stable A |] \
-\     ==> F : Stable (extend_set h A)";
+     "[| reachable (extend h F Join G) <= C;  \
+\        F Join project C h G : Stable A |]   \
+\     ==> extend h F Join G : Stable (extend_set h A)";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
 qed "project_Stable_D";
 
 Goalw [Always_def]
-     "[| reachable F <= C;  project C h F : Always A |] \
-\     ==> F : Always (extend_set h A)";
+     "[| reachable (extend h F Join G) <= C;  \
+\        F Join project C h G : Always A |]   \
+\     ==> extend h F Join G : Always (extend_set h A)";
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
 	       simpset() addsimps [project_Stable_D]) 1);
 qed "project_Always_D";
 
 Goalw [Increasing_def]
-     "[| reachable F <= C;  project C h F : Increasing func |] \
-\     ==> F : Increasing (func o f)";
+     "[| reachable (extend h F Join G) <= C;  \
+\        F Join project C h G : Increasing func |] \
+\     ==> extend h F Join G : Increasing (func o f)";
 by Auto_tac;
 by (stac Collect_eq_extend_set 1);
 by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
@@ -504,71 +526,71 @@
 
 (** Converse results for weak safety: benefits of the argument C *)
 
-Goal "[| C <= reachable F; x : reachable (project C h F) |] \
-\     ==> EX y. h(x,y) : reachable F";
+Goal "[| C <= reachable(extend h F Join G);   \
+\        x : reachable (F Join project C h G) |] \
+\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
 by (etac reachable.induct 1);
-by (ALLGOALS 
-    (asm_full_simp_tac
-     (simpset() addsimps [project_set_def, project_act_def])));
-by (force_tac (claset() addIs [reachable.Acts],
+by (ALLGOALS Asm_full_simp_tac);
+(*SLOW: 6.7s*)
+by (force_tac (claset() delrules [Id_in_Acts]
+		        addIs [reachable.Acts, extend_act_D],
 	       simpset() addsimps [project_act_def]) 2);
 by (force_tac (claset() addIs [reachable.Init],
 	       simpset() addsimps [project_set_def]) 1);
 qed "reachable_project_imp_reachable";
 
 Goalw [Constrains_def]
-     "[| C <= reachable F;  F : (extend_set h A) Co (extend_set h B) |] \
-\     ==> project C h F : A Co B";
-by (full_simp_tac (simpset() addsimps [project_constrains, 
+     "[| C <= reachable (extend h F Join G);  \
+\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
+\     ==> F Join project C h G : A Co B";
+by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
-by (force_tac (claset() addSDs [constrains_imp_subset, 
-				reachable_project_imp_reachable], 
-	       simpset()) 2);
 by (etac constrains_weaken 1);
 by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
+(*Some generalization of constrains_weaken_L would be better, but what is it?*)
+by (rewtac constrains_def);
+by Auto_tac;
+by (thin_tac "ALL act : Acts G. ?P act" 1);
+by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
+	       simpset()) 1);
 qed "project_Constrains_I";
 
 Goalw [Stable_def]
-     "[| C <= reachable F;  F : Stable (extend_set h A) |] \
-\     ==> project C h F : Stable A";
+     "[| C <= reachable (extend h F Join G);  \
+\        extend h F Join G : Stable (extend_set h A) |] \
+\     ==> F Join project C h G : Stable A";
 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
 qed "project_Stable_I";
 
 Goalw [Increasing_def]
-     "[| C <= reachable F;  F : Increasing (func o f) |] \
-\     ==> project C h F : Increasing func";
+     "[| C <= reachable (extend h F Join G);  \
+\        extend h F Join G : Increasing (func o f) |] \
+\     ==> F Join project C h G : Increasing func";
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
 				      project_Stable_I]) 1); 
 qed "project_Increasing_I";
 
-Goal "(project (reachable F) h F : A Co B)  =  \
-\     (F : (extend_set h A) Co (extend_set h B))";
+Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
+\     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
 by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
 qed "project_Constrains";
 
 Goalw [Stable_def]
-     "(project (reachable F) h F : Stable A)  =  \
-\     (F : Stable (extend_set h A))";
+     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
+\     (extend h F Join G : Stable (extend_set h A))";
 by (rtac project_Constrains 1);
 qed "project_Stable";
 
-Goal "(project (reachable F) h F : Increasing func)  =  \
-\     (F : Increasing (func o f))";
+Goal
+   "(F Join project (reachable (extend h F Join G)) h 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);
 qed "project_Increasing";
 
-(**
-    (*NOT useful in its own right, but a guarantees rule likes premises
-      in this form*)
-    Goal "F Join project C h G : A Co B    \
-    \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-    by (asm_simp_tac
-	(simpset() addsimps [project_extend_Join, project_Constrains_D]) 1);
-    qed "extend_Join_Constrains";
-**)
 
 (*** Progress: transient, ensures ***)
 
@@ -714,16 +736,14 @@
 Goal "F : UNIV guarantees increasing func \
 \     ==> extend h F : UNIV guarantees increasing (func o f)";
 by (etac project_guarantees 1);
-by (asm_simp_tac (simpset() addsimps [project_increasing RS sym]) 2);
-by (stac (project_set_UNIV RS project_extend_Join) 2);
-by Auto_tac;
+by (ALLGOALS
+    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
 qed "extend_guar_increasing";
 
 Goal "F : UNIV guarantees Increasing func \
 \     ==> extend h F : UNIV guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
 by (rtac (subset_UNIV RS project_Increasing_D) 2);
-by (stac (project_set_UNIV RS project_extend_Join) 2);
 by Auto_tac;
 qed "extend_guar_Increasing";
 
@@ -733,9 +753,7 @@
 by (etac project_guarantees 1);
 (*the "increasing" guarantee*)
 by (asm_simp_tac
-    (simpset() addsimps [project_increasing RS sym]) 2);
-by (stac (project_set_UNIV RS project_extend_Join) 2);
-by (assume_tac 2);
+    (simpset() addsimps [Join_project_increasing RS sym]) 2);
 (*the "localTo" requirement*)
 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
 by (asm_simp_tac 
@@ -747,9 +765,7 @@
 \                      guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
 (*the "Increasing" guarantee*)
-by (rtac (subset_UNIV RS project_Increasing_D) 2);
-by (stac (project_set_UNIV RS project_extend_Join) 2);
-by (assume_tac 2);
+by (etac (subset_UNIV RS project_Increasing_D) 2);
 (*the "localTo" requirement*)
 by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
 by (asm_simp_tac 

--- a/src/HOL/UNITY/PPROD.ML	Fri Sep 10 18:40:06 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Fri Sep 17 10:31:38 1999 +0200
@@ -64,10 +64,17 @@
 
 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";
+by (auto_tac (claset(), 
+	      simpset() addsimps [ensures_def, lift_prog_transient_eq_disj]));
+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";
-by (rtac (ensuresI RS leadsTo_Basis) 1);
-by (auto_tac (claset(), simpset() addsimps [lift_prog_transient_eq_disj]));
+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 |] \