src/HOL/UNITY/WFair.thy
 author berghofe Wed Oct 21 17:57:02 1998 +0200 (1998-10-21) changeset 5721 458a67fd5461 parent 5648 fe887910e32e child 5931 325300576da7 permissions -rw-r--r--
Changed interface of inductive.
```     1 (*  Title:      HOL/UNITY/WFair
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1998  University of Cambridge
```
```     5
```
```     6 Weak Fairness versions of transient, ensures, leadsTo.
```
```     7
```
```     8 From Misra, "A Logic for Concurrent Programming", 1994
```
```     9 *)
```
```    10
```
```    11 WFair = UNITY +
```
```    12
```
```    13 constdefs
```
```    14
```
```    15   (*This definition specifies weak fairness.  The rest of the theory
```
```    16     is generic to all forms of fairness.*)
```
```    17   transient :: "'a set => 'a program set"
```
```    18     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
```
```    19
```
```    20   ensures :: "['a set, 'a set] => 'a program set"
```
```    21     "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
```
```    22
```
```    23
```
```    24 consts leadsto :: "'a program => ('a set * 'a set) set"
```
```    25
```
```    26 inductive "leadsto F"
```
```    27   intrs
```
```    28
```
```    29     Basis  "F : ensures A B ==> (A,B) : leadsto F"
```
```    30
```
```    31     Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
```
```    32 	   ==> (A,C) : leadsto F"
```
```    33
```
```    34     (*Encoding using powerset of the desired axiom
```
```    35        (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
```
```    36     *)
```
```    37     Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
```
```    38
```
```    39   monos Pow_mono
```
```    40
```
```    41
```
```    42
```
```    43 constdefs (*visible version of the relation*)
```
```    44   leadsTo :: "['a set, 'a set] => 'a program set"
```
```    45     "leadsTo A B == {F. (A,B) : leadsto F}"
```
```    46
```
```    47   (*wlt F B is the largest set that leads to B*)
```
```    48   wlt :: "['a program, 'a set] => 'a set"
```
```    49     "wlt F B == Union {A. F: leadsTo A B}"
```
```    50
```
```    51 end
```