src/HOL/UNITY/Comp.thy
 author paulson Thu Aug 26 11:39:18 1999 +0200 (1999-08-26) changeset 7364 a979e8a2ee18 parent 6822 8932f33259d4 child 7399 cf780c2bcccf permissions -rw-r--r--
changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE
```     1 (*  Title:      HOL/UNITY/Comp.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1998  University of Cambridge
```
```     5
```
```     6 Composition
```
```     7
```
```     8 From Chandy and Sanders, "Reasoning About Program Composition"
```
```     9 *)
```
```    10
```
```    11 Comp = Union +
```
```    12
```
```    13 constdefs
```
```    14
```
```    15   (*Existential and Universal properties.  I formalize the two-program
```
```    16     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
```
```    17
```
```    18   ex_prop  :: 'a program set => bool
```
```    19    "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
```
```    20
```
```    21   strict_ex_prop  :: 'a program set => bool
```
```    22    "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
```
```    23
```
```    24   uv_prop  :: 'a program set => bool
```
```    25    "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
```
```    26
```
```    27   strict_uv_prop  :: 'a program set => bool
```
```    28    "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
```
```    29
```
```    30   (*Ill-defined programs can arise through "Join"*)
```
```    31   welldef :: 'a program set
```
```    32    "welldef == {F. Init F ~= {}}"
```
```    33
```
```    34   component :: ['a program, 'a program] => bool     (infixl 50)
```
```    35    "F component H == EX G. F Join G = H"
```
```    36
```
```    37   guar :: ['a program set, 'a program set] => 'a program set
```
```    38    (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
```
```    39    "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
```
```    40
```
```    41   refines :: ['a program, 'a program, 'a program set] => bool
```
```    42 			("(3_ refines _ wrt _)" [10,10,10] 10)
```
```    43    "G refines F wrt X ==
```
```    44       ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
```
```    45
```
```    46   iso_refines :: ['a program, 'a program, 'a program set] => bool
```
```    47 			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
```
```    48    "G iso_refines F wrt X ==
```
```    49       F : welldef Int X --> G : welldef Int X"
```
```    50
```
```    51 end
```