# HG changeset patch
# User paulson
# Date 927792832 -7200
# Node ID 06189132c67b4662cf965b5d74ed569945046759
# Parent  03f0ff7ee02921204b10f9b9a4592e223c5511f5
component_eq_subset: a neat characterization of "component"

diff -r 03f0ff7ee029 -r 06189132c67b src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed May 26 22:45:59 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Thu May 27 10:13:52 1999 +0200
@@ -10,6 +10,12 @@
 
 (*** component ***)
 
+Goalw [component_def]
+     "(F component G) = (Init G <= Init F & Acts F <= Acts G)";
+by (force_tac (claset() addSIs [exI, program_equalityI], 
+	       simpset() addsimps [Acts_Join]) 1);
+qed "component_eq_subset";
+
 Goalw [component_def] "SKIP component F";
 by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
 qed "component_SKIP";
@@ -37,17 +43,9 @@
 by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
 qed "component_trans";
 
-Goalw [component_def] "F component G ==> Acts F <= Acts G";
-by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
-qed "component_Acts";
-
-Goalw [component_def,Join_def] "F component G ==> Init G <= Init F";
-by Auto_tac;
-qed "component_Init";
-
 Goal "[| F component G; G component F |] ==> F=G";
-by (blast_tac (claset() addSIs [program_equalityI, 
-				component_Init, component_Acts]) 1);
+by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (blast_tac (claset() addSIs [program_equalityI]) 1);
 qed "component_antisym";
 
 Goalw [component_def]