# HG changeset patch
# User paulson
# Date 908269534 -7200
# Node ID 4a59d99b5ca3e378806e01ddc05d6a97d8a6ace1
# Parent  29d8e53a4920e3380cb5750986135d8c73591874
new theorems

diff -r 29d8e53a4920 -r 4a59d99b5ca3 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Tue Oct 13 10:55:33 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Tue Oct 13 11:05:34 1998 +0200
@@ -72,6 +72,12 @@
 				      stable_constrains_Int]) 1);
 qed "stable_ensures_Int";
 
+Goal "[| stable acts A;  transient acts C;  A <= B Un C |] \
+\     ==> ensures acts A B";
+by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
+by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
+qed "stable_transient_ensures";
+
 
 (*** leadsTo ***)
 
@@ -79,6 +85,11 @@
 bind_thm ("leadsTo_Basis", leadsto.Basis);
 bind_thm ("leadsTo_Trans", leadsto.Trans);
 
+Goal "transient acts A ==> leadsTo acts A (-A)";
+by (asm_simp_tac 
+    (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
+qed "transient_imp_leadsTo";
+
 Goal "act: acts ==> leadsTo acts A UNIV";
 by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
 qed "leadsTo_UNIV";
@@ -264,7 +275,7 @@
 
 (** PSP: Progress-Safety-Progress **)
 
-(*Special case of PSP: Misra's "stable conjunction".  Doesn't need Id:acts. *)
+(*Special case of PSP: Misra's "stable conjunction"*)
 Goalw [stable_def]
    "[| leadsTo acts A A'; stable acts B |] \
 \   ==> leadsTo acts (A Int B) (A' Int B)";