src/ZF/UNITY/WFair.thy

--- a/src/ZF/UNITY/WFair.thy	Wed Nov 14 23:22:43 2001 +0100
+++ b/src/ZF/UNITY/WFair.thy	Thu Nov 15 15:07:16 2001 +0100
@@ -13,11 +13,11 @@
 WFair = UNITY +
 constdefs
   
-  (*This definition specifies weak fairness.  The rest of the theory
+  (* This definition specifies weak fairness.  The rest of the theory
     is generic to all forms of fairness.*) 
  transient :: "i=>i"
-  "transient(A) =={F:program. (EX act: Acts(F). 
-			       A<= domain(act) & act``A <= state-A) & A:condition}"
+  "transient(A) =={F:program. (EX act: Acts(F). A<=domain(act) &
+			       act``A <= state-A) & st_set(A)}"
 
   ensures :: "[i,i] => i"       (infixl 60)
   "A ensures B == ((A-B) co (A Un B)) Int transient(A-B)"
@@ -25,31 +25,29 @@
 consts
 
   (*LEADS-TO constant for the inductive definition*)
-  leads :: "i=>i"
+  leads :: "[i, i]=>i"
 
-inductive (* All typing conidition `A:condition' will desapear
-             in the dervied rules *)
+inductive 
   domains
-     "leads(F)" <= "condition*condition"
+     "leads(D, F)" <= "Pow(D)*Pow(D)"
   intrs 
-    Basis  "[| F:A ensures B; A:condition; B:condition |] ==> <A,B>:leads(F)"
-    Trans  "[| <A,B> : leads(F); <B,C> : leads(F) |] ==>  <A,C>:leads(F)"
-    Union   "[| S:Pow({A:S. <A, B>:leads(F)});
-		B:condition; S:Pow(condition) |] ==> 
-	      <Union(S),B>:leads(F)"
+    Basis  "[| F:A ensures B;  A:Pow(D); B:Pow(D) |] ==> <A,B>:leads(D, F)"
+    Trans  "[| <A,B> : leads(D, F); <B,C> : leads(D, F) |] ==>  <A,C>:leads(D, F)"
+    Union   "[| S:Pow({A:S. <A, B>:leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==> 
+	      <Union(S),B>:leads(D, F)"
 
   monos        Pow_mono
-  type_intrs  "[UnionI, Union_in_conditionI, PowI]"
+  type_intrs  "[Union_PowI, UnionI, PowI]"
  
 constdefs
 
-  (*visible version of the LEADS-TO relation*)
+  (* The Visible version of the LEADS-TO relation*)
   leadsTo :: "[i, i] => i"       (infixl 60)
-    "A leadsTo B == {F:program.  <A,B>:leads(F)}"
+  "A leadsTo B == {F:program. <A,B>:leads(state, F)}"
   
-  (*wlt F B is the largest set that leads to B*)
+  (* wlt(F, B) is the largest set that leads to B*)
   wlt :: "[i, i] => i"
-    "wlt(F, B) == Union({A:condition. F: A leadsTo B})"
+    "wlt(F, B) == Union({A:Pow(state). F: A leadsTo B})"
 
 syntax (xsymbols)
   "op leadsTo" :: "[i, i] => i" (infixl "\\<longmapsto>" 60)