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