src/HOL/UNITY/Comp.thy
author paulson
Mon Mar 01 18:38:43 1999 +0100 (1999-03-01)
changeset 6295 351b3c2b0d83
parent 6138 b7e6e607bb4d
child 6646 3ea726909fff
permissions -rw-r--r--
removed the infernal States, eqStates, compatible, etc.
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@5597
     9
*)
paulson@5597
    10
paulson@5597
    11
Comp = Union +
paulson@5597
    12
paulson@5597
    13
constdefs
paulson@5597
    14
paulson@5597
    15
  (*Existential and Universal properties.  I formalize the two-program
paulson@5597
    16
    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
paulson@5597
    17
paulson@5597
    18
  ex_prop  :: 'a program set => bool
paulson@6295
    19
   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
paulson@5597
    20
paulson@5597
    21
  strict_ex_prop  :: 'a program set => bool
paulson@6295
    22
   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
paulson@5597
    23
paulson@5597
    24
  uv_prop  :: 'a program set => bool
paulson@6295
    25
   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
paulson@5597
    26
paulson@5597
    27
  strict_uv_prop  :: 'a program set => bool
paulson@6295
    28
   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
paulson@5597
    29
paulson@5612
    30
  (*Ill-defined programs can arise through "Join"*)
paulson@5612
    31
  welldef :: 'a program set  
paulson@5612
    32
   "welldef == {F. Init F ~= {}}"
paulson@5597
    33
paulson@5597
    34
  component :: ['a program, 'a program] => bool
paulson@6295
    35
   "component F H == EX G. F Join G = H"
paulson@5597
    36
paulson@5597
    37
  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
paulson@5597
    38
   "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
paulson@5597
    39
paulson@5612
    40
  refines :: ['a program, 'a program, 'a program set] => bool
paulson@5612
    41
			("(3_ refines _ wrt _)" [10,10,10] 10)
paulson@5612
    42
   "G refines F wrt X ==
paulson@6295
    43
      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
paulson@5612
    44
paulson@5612
    45
  iso_refines :: ['a program, 'a program, 'a program set] => bool
paulson@5612
    46
			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
paulson@5612
    47
   "G iso_refines F wrt X ==
paulson@5612
    48
      F : welldef Int X --> G : welldef Int X"
paulson@5612
    49
paulson@5597
    50
end