src/HOL/UNITY/Comp.ML

 Goal "[| component F G; component G F |] ==> F=G";
 by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
 				      component_Acts, component_Init]) 1);
 qed "component_anti_sym";
 
+Goalw [component_def]
+      "component F H = (EX G. F Join G = H & Disjoint F G)";
+by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
+qed "component_eq";
 
 (*** existential properties ***)
 
 Goalw [ex_prop_def]
      "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";

 
 
 (*** guarantees ***)
 
 (*This equation is more intuitive than the official definition*)
-Goalw [guarantees_def, component_def]
-      "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
+Goal "(F : A guarantees B) = \
+\     (ALL G. F Join G : A & Disjoint F G --> F Join G : B)";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (Blast_tac 1);
 qed "guarantees_eq";
 
 Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
 by (Blast_tac 1);

 Goalw [guarantees_def]
      "EX z:I. F : A guarantees (B z) ==> F : A guarantees (UN z:I. B z)";
 by (Blast_tac 1);
 qed "ex_guarantees";
 
-val prems = Goalw [guarantees_def, component_def]
-      "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
+val prems = Goal
+     "(!!G. [| F Join G : A;  Disjoint F G |] ==> F Join G : B) \
+\     ==> F : A guarantees B";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
-Goal "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
-by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1);
+Goalw [guarantees_def, component_def]
+     "[| F : A guarantees B;  F Join G : A |] ==> F Join G : B";
+by (Blast_tac 1);
 qed "guaranteesD";
 
 
 (*** well-definedness ***)