src/HOL/UNITY/Union.ML
changeset 5867 1c4806b4bf43
parent 5804 8e0a4c4fd67b
child 5898 3e34e7aa7479
--- 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];
-