src/HOL/UNITY/Comp.thy
author paulson
Thu Dec 03 10:45:06 1998 +0100 (1998-12-03)
changeset 6012 1894bfc4aee9
parent 5612 e981ca6f7332
child 6138 b7e6e607bb4d
permissions -rw-r--r--
Addition of the States component; parts of Comp not working
     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 ==
    20       ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
    21 
    22   strict_ex_prop  :: 'a program set => bool
    23    "strict_ex_prop X ==
    24       ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
    25 
    26   uv_prop  :: 'a program set => bool
    27    "uv_prop X ==
    28       SKIP UNIV : X &
    29       (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
    30 
    31   strict_uv_prop  :: 'a program set => bool
    32    "strict_uv_prop X ==
    33       SKIP UNIV : X &
    34       (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
    35 
    36   (*Ill-defined programs can arise through "Join"*)
    37   welldef :: 'a program set  
    38    "welldef == {F. Init F ~= {}}"
    39 
    40   component :: ['a program, 'a program] => bool
    41    "component F H == EX G. F Join G = H & States F = States G"
    42 
    43   guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    44    "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
    45 
    46   refines :: ['a program, 'a program, 'a program set] => bool
    47 			("(3_ refines _ wrt _)" [10,10,10] 10)
    48    "G refines F wrt X ==
    49       States F = States G &
    50       (ALL H. States F = States H & (F Join H) : welldef Int X
    51         --> G Join H : welldef Int X)"
    52 
    53   iso_refines :: ['a program, 'a program, 'a program set] => bool
    54 			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    55    "G iso_refines F wrt X ==
    56       F : welldef Int X --> G : welldef Int X"
    57 
    58 end