src/HOL/UNITY/Comp.thy
author paulson
Tue Jan 19 11:15:40 1999 +0100 (1999-01-19)
changeset 6138 b7e6e607bb4d
parent 6012 1894bfc4aee9
child 6295 351b3c2b0d83
permissions -rw-r--r--
updated comments
paulson@5597
     1
(*  Title:      HOL/UNITY/Comp.thy
paulson@5597
     2
    ID:         $Id$
paulson@5597
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5597
     4
    Copyright   1998  University of Cambridge
paulson@5597
     5
paulson@5597
     6
Composition
paulson@5597
     7
paulson@5597
     8
From Chandy and Sanders, "Reasoning About Program Composition"
paulson@6138
     9
paulson@6138
    10
QUESTIONS:
paulson@6138
    11
  refines_def: needs the States F = States G?
paulson@6138
    12
paulson@6138
    13
  uv_prop, component: should be States F = States (F Join G)
paulson@5597
    14
*)
paulson@5597
    15
paulson@5597
    16
Comp = Union +
paulson@5597
    17
paulson@5597
    18
constdefs
paulson@5597
    19
paulson@5597
    20
  (*Existential and Universal properties.  I formalize the two-program
paulson@5597
    21
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
paulson@5597
    22
paulson@5597
    23
  ex_prop  :: 'a program set => bool
paulson@6012
    24
   "ex_prop X ==
paulson@6012
    25
      ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
paulson@5597
    26
paulson@5597
    27
  strict_ex_prop  :: 'a program set => bool
paulson@6012
    28
   "strict_ex_prop X ==
paulson@6012
    29
      ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
paulson@5597
    30
paulson@5597
    31
  uv_prop  :: 'a program set => bool
paulson@6012
    32
   "uv_prop X ==
paulson@6012
    33
      SKIP UNIV : X &
paulson@6012
    34
      (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
paulson@5597
    35
paulson@5597
    36
  strict_uv_prop  :: 'a program set => bool
paulson@6012
    37
   "strict_uv_prop X ==
paulson@6012
    38
      SKIP UNIV : X &
paulson@6012
    39
      (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
paulson@5597
    40
paulson@5612
    41
  (*Ill-defined programs can arise through "Join"*)
paulson@5612
    42
  welldef :: 'a program set  
paulson@5612
    43
   "welldef == {F. Init F ~= {}}"
paulson@5597
    44
paulson@5597
    45
  component :: ['a program, 'a program] => bool
paulson@6012
    46
   "component F H == EX G. F Join G = H & States F = States G"
paulson@5597
    47
paulson@5597
    48
  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
paulson@5597
    49
   "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
paulson@5597
    50
paulson@5612
    51
  refines :: ['a program, 'a program, 'a program set] => bool
paulson@5612
    52
			("(3_ refines _ wrt _)" [10,10,10] 10)
paulson@5612
    53
   "G refines F wrt X ==
paulson@6012
    54
      States F = States G &
paulson@6012
    55
      (ALL H. States F = States H & (F Join H) : welldef Int X
paulson@6012
    56
        --> G Join H : welldef Int X)"
paulson@5612
    57
paulson@5612
    58
  iso_refines :: ['a program, 'a program, 'a program set] => bool
paulson@5612
    59
			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
paulson@5612
    60
   "G iso_refines F wrt X ==
paulson@5612
    61
      F : welldef Int X --> G : welldef Int X"
paulson@5612
    62
paulson@5597
    63
end