src/HOL/UNITY/Union.ML

--- a/src/HOL/UNITY/Union.ML	Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Fri Sep 10 18:40:06 1999 +0200
@@ -58,7 +58,7 @@
 by (auto_tac (claset(), simpset() addsimps [Join_def]));
 qed "Acts_Join";
 
-Addsimps [Init_Join];
+Addsimps [Init_Join, Acts_Join];
 
 
 (** JN **)
@@ -82,7 +82,7 @@
 by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
 qed "Acts_JN";
 
-Addsimps [Init_JN];
+Addsimps [Init_JN, Acts_JN];
 
 val prems = Goalw [JOIN_def]
     "[| I=J;  !!i. i:J ==> F i = G i |] ==> \
@@ -139,23 +139,19 @@
 
 (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
 Goal "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
 qed "JN_absorb";
 
 Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
 qed "JN_Un";
 
 Goal "(JN i:I. c) = (if I={} then SKIP else c)";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Acts_JN]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
 qed "JN_constant";
 
 Goal "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
 qed "JN_Join_distrib";
 
 Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)";
@@ -268,7 +264,7 @@
 by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, 
 				       Stable_eq_stable, Join_stable]) 1);
 by (force_tac(claset() addIs [stable_reachable, stable_Int],
-	      simpset() addsimps [Acts_Join]) 1);
+	      simpset()) 1);
 qed "stable_Join_Always";
 
 Goal "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B";
@@ -300,7 +296,7 @@
 \     ==> G : (INT z. stable {s. v s = z})";
 by (asm_full_simp_tac 
     (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
-			 Acts_Join, stable_def, constrains_def]) 1);
+			 stable_def, constrains_def]) 1);
 by (Blast_tac 1);
 qed "localTo_imp_stable";
 
@@ -308,7 +304,7 @@
 \        act : Acts G;  Disjoint F G |] ==> v s' = v s";
 by (asm_full_simp_tac 
     (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
-			 Acts_Join, stable_def, constrains_def]) 1);
+			 stable_def, constrains_def]) 1);
 by (Blast_tac 1);
 qed "localTo_imp_equals";
 
@@ -326,7 +322,7 @@
 \        F Join G : w localTo F;       \
 \        Disjoint F G |]               \
 \     ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
 by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
 by Auto_tac;
 qed "constrains_localTo_constrains2";