UNITY fully working at last...

--- a/src/HOL/UNITY/Comp.ML	Wed Mar 03 10:36:24 1999 +0100
+++ b/src/HOL/UNITY/Comp.ML	Wed Mar 03 10:50:42 1999 +0100
@@ -181,7 +181,7 @@
 qed "guaranteesI";
 
 Goalw [guarantees_def, component_def]
-     "[| F : X guarantees Y;  F Join G : X;  compatible{F,G} |] \
+     "[| F : X guarantees Y;  F Join G : X |] \
 \     ==> F Join G : Y";
 by (Blast_tac 1);
 qed "guaranteesD";

--- a/src/HOL/UNITY/PPROD.ML	Wed Mar 03 10:36:24 1999 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Wed Mar 03 10:50:42 1999 +0100
@@ -21,7 +21,13 @@
 qed "lift_act_Id";
 Addsimps [lift_act_Id];
 
-Goalw [lift_prog_def] "Init (lift_prog i F) = {f. f i : Init F}";
+(*NEEDED????????????????????????????????????????????????????????????????*)
+Goal "Id : lift_act i `` Acts F";
+by (auto_tac (claset() addSIs [lift_act_Id RS sym], 
+	      simpset() addsimps [image_iff]));
+qed "Id_mem_lift_act";
+
+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];
@@ -41,25 +47,20 @@
 qed "lift_act_eq";
 AddIffs [lift_act_eq];
 
-Goal "i: I ==> Acts (PPROD I F) = (UN i:I. lift_act i `` Acts (F i))";
+Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
 by (auto_tac (claset(),
 	      simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN]));
 qed "Acts_PPROD";
 
-Goal "PPROD {} F = SKIP UNIV";
-by (simp_tac (simpset() addsimps [PPROD_def]) 1);
-qed "Acts_PPROD";
-
-Goal "i : I ==> (PPI i: I. SKIP A) = SKIP (INT i:I. lift_set i A)";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [eqStates_def, Acts_lift_prog, 
-				  SKIP_def, Acts_PPROD]));
-qed "PPROD_SKIP";
-
 Goal "PPROD {} F = SKIP";
 by (simp_tac (simpset() addsimps [PPROD_def]) 1);
 qed "PPROD_empty";
 
+Goal "(PPI i: I. SKIP) = SKIP";
+by (auto_tac (claset() addSIs [program_equalityI],
+	      simpset() addsimps [Acts_lift_prog, SKIP_def, Acts_PPROD]));
+qed "PPROD_SKIP";
+
 Addsimps [PPROD_SKIP, PPROD_empty];
 
 Goalw [PPROD_def]
@@ -132,18 +133,21 @@
 
 (** invariant **)
 
+(*????????????????*)
 Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
 qed "invariant_imp_lift_prog_invariant";
 
+(*????????????????*)
 Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
 qed "lift_prog_invariant_imp_invariant";
 
 (*NOT clear that the previous lemmas help in proving this one.*)
-Goal "[| F i : invariant A;  i : I |] ==> PPROD I F : invariant (lift_set i A)";
+Goal "[| F i : invariant A;  i : I |] \
+\     ==> PPROD I F : invariant (lift_set i A)";
 by (auto_tac (claset(),
 	      simpset() addsimps [invariant_def, PPROD_stable]));
 qed "invariant_imp_PPROD_invariant";
@@ -248,10 +252,10 @@
 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
 qed "Constrains_imp_PPROD_Constrains";
 
-Goal "[| ALL i:I. f0 i : R i;  i: I |] \
-\     ==> Applyall {f. (ALL i:I. f i : R i) & f i : A} i = R i Int A";
-by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI],
-	       simpset() addsimps [Applyall_def]) 1);
+Goal "[| ALL i:I. f0 i : R i;   i: I |] \
+\     ==> Applyall ({f. (ALL i:I. f i : R i)} Int lift_set i A) i = R i Int A";
+by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
+	       simpset() addsimps [Applyall_def, lift_set_def]) 1);
 qed "Applyall_Int_depend";
 
 (*Again, we need the f0 premise because otherwise Constrains holds trivially
@@ -265,8 +269,7 @@
 by (dtac PPROD_constrains_projection 1);
 by (assume_tac 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [Applyall_Int_depend, Collect_conj_eq RS sym,
-			 reachable_PPROD_eq]) 1);
+    (simpset() addsimps [Applyall_Int_depend, reachable_PPROD_eq]) 1);
 qed "PPROD_Constrains_imp_Constrains";
 
 
@@ -286,7 +289,8 @@
 
 (** PFUN (no dependence on i) doesn't require the f0 premise **)
 
-Goal "i: I ==> Applyall {f. (ALL i:I. f i : R) & f i : A} i = R Int A";
+Goal "i: I \
+\     ==> Applyall ({f. (ALL i:I. f i : R)} Int lift_set i A) i = R Int A";
 by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1);
 qed "Applyall_Int";
 

--- a/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:36:24 1999 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Wed Mar 03 10:50:42 1999 +0100
@@ -28,10 +28,8 @@
 time_use_thy "Lift";
 time_use_thy "Comp";
 time_use_thy "Client";
-(**
 time_use_thy "Extend";
 time_use_thy "PPROD";
-**)
 
 add_path "../Auth";	(*to find Public.thy*)
 use_thy"NSP_Bad";

--- a/src/HOL/UNITY/Union.ML	Wed Mar 03 10:36:24 1999 +0100
+++ b/src/HOL/UNITY/Union.ML	Wed Mar 03 10:50:42 1999 +0100
@@ -167,12 +167,6 @@
 by (Blast_tac 1);
 qed "constrains_imp_JN_constrains";
 
-Goal "[| i : I;  compatible (F``I) |] \
-\     ==> (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
-by (asm_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
-by (Blast_tac 1);
-qed "constrains_JN";
-
     (**FAILS, I think; see 5.4.1, Substitution Axiom.
        The problem is to relate reachable (F Join G) with 
        reachable F and reachable G