# HG changeset patch
# User paulson
# Date 911209170 -3600
# Node ID 1c4806b4bf43c3571060d25c1f589f8f8e08fea1
# Parent  de6a1856c74ad507dfe716a16efb8f81d56314a3
generalized JN_empty and added reachable_SKIP

diff -r de6a1856c74a -r 1c4806b4bf43 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Nov 16 10:37:54 1998 +0100
+++ b/src/HOL/UNITY/Union.ML	Mon Nov 16 10:39:30 1998 +0100
@@ -9,6 +9,8 @@
 *)
 
 
+(** SKIP **)
+
 Goal "Init SKIP = UNIV";
 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
 qed "Init_SKIP";
@@ -19,6 +21,15 @@
 
 Addsimps [Init_SKIP, Acts_SKIP];
 
+Goal "reachable SKIP = UNIV";
+by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
+qed "reachable_SKIP";
+
+Addsimps [reachable_SKIP];
+
+
+(** Join and JN **)
+
 Goal "Init (F Join G) = Init F Int Init G";
 by (simp_tac (simpset() addsimps [Join_def]) 1);
 qed "Init_Join";
@@ -37,11 +48,15 @@
 
 Addsimps [Init_Join, Init_JN];
 
+Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
+by Auto_tac;
+qed "JN_empty";
+
 Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
 by (rtac program_equalityI 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
 qed "JN_insert";
-Addsimps[JN_insert];
+Addsimps[JN_empty, JN_insert];
 
 
 (** Algebraic laws **)
@@ -73,11 +88,6 @@
 
 Addsimps [Join_absorb];
 
-Goal "(JN G:{}. G) = SKIP";
-by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
-qed "JN_empty";
-Addsimps [JN_empty];
-