src/HOL/UNITY/WFair.thy
 changeset 5648 fe887910e32e parent 5340 d75c03cf77b5 child 5721 458a67fd5461
```--- a/src/HOL/UNITY/WFair.thy	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Oct 15 11:35:07 1998 +0200
@@ -14,39 +14,38 @@

(*This definition specifies weak fairness.  The rest of the theory
is generic to all forms of fairness.*)
-  transient :: "[('a * 'a)set set, 'a set] => bool"
-    "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"
-
-  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
-    "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
-			(*(unless acts A B) would be equivalent*)
+  transient :: "'a set => 'a program set"
+    "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"

-syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
-consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+  ensures :: "['a set, 'a set] => 'a program set"
+    "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
+
+
+consts leadsto :: "'a program => ('a set * 'a set) set"

-translations
-
intrs

-    Basis  "ensures acts A B ==> leadsTo acts A B"
+    Basis  "F : ensures A B ==> (A,B) : leadsto F"

-    Trans  "[| leadsTo acts A B;  leadsTo acts B C |]
-	   ==> leadsTo acts A C"
+    Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
+	   ==> (A,C) : leadsto F"

(*Encoding using powerset of the desired axiom
-       (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
+       (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
*)
-    Union  "(UN A:S. {(A,B)}) : Pow (leadsto acts)
-	   ==> leadsTo acts (Union S) B"
+    Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"

monos "[Pow_mono]"

-(*wlt acts B is the largest set that leads to B*)
-constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
-  "wlt acts B == Union {A. leadsTo acts A B}"
+
+constdefs (*visible version of the relation*)
+  leadsTo :: "['a set, 'a set] => 'a program set"