--- 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];
-