src/HOL/UNITY/WFair.thy
 changeset 6536 281d44905cab parent 5931 325300576da7 child 6801 9e0037839d63
```--- a/src/HOL/UNITY/WFair.thy	Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Apr 29 10:51:58 1999 +0200
@@ -17,16 +17,22 @@
transient :: "'a set => 'a program set"
"transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"

-  ensures :: "['a set, 'a set] => 'a program set"
-    "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
+
+consts
+
+  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)

+  (*LEADS-TO constant for the inductive definition*)
+  leadsto :: "'a program => ('a set * 'a set) set"

-consts leadsto :: "'a program => ('a set * 'a set) set"
+  (*visible version of the LEADS-TO relation*)
+  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
+

inductive "leadsto F"
intrs

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

Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
==> (A,C) : leadsto F"
@@ -40,12 +46,15 @@

-constdefs (*visible version of the relation*)
-  leadsTo :: "['a set, 'a set] => 'a program set"
-    "leadsTo A B == {F. (A,B) : leadsto F}"
+defs
+  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
+
+  leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
+
+constdefs

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

end```