src/HOL/UNITY/Comp.thy
changeset 7399 cf780c2bcccf
parent 7364 a979e8a2ee18
child 8055 bb15396278fb
     1.1 --- a/src/HOL/UNITY/Comp.thy	Mon Aug 30 23:19:13 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Tue Aug 31 15:56:56 1999 +0200
     1.3 @@ -10,42 +10,13 @@
     1.4  
     1.5  Comp = Union +
     1.6  
     1.7 -constdefs
     1.8 -
     1.9 -  (*Existential and Universal properties.  I formalize the two-program
    1.10 -    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    1.11 -
    1.12 -  ex_prop  :: 'a program set => bool
    1.13 -   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
    1.14 -
    1.15 -  strict_ex_prop  :: 'a program set => bool
    1.16 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
    1.17 -
    1.18 -  uv_prop  :: 'a program set => bool
    1.19 -   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
    1.20 -
    1.21 -  strict_uv_prop  :: 'a program set => bool
    1.22 -   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
    1.23 +instance
    1.24 +  program :: (term)ord
    1.25  
    1.26 -  (*Ill-defined programs can arise through "Join"*)
    1.27 -  welldef :: 'a program set  
    1.28 -   "welldef == {F. Init F ~= {}}"
    1.29 -
    1.30 -  component :: ['a program, 'a program] => bool     (infixl 50)
    1.31 -   "F component H == EX G. F Join G = H"
    1.32 +defs
    1.33  
    1.34 -  guar :: ['a program set, 'a program set] => 'a program set
    1.35 -   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
    1.36 -   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
    1.37 +  component_def   "F <= H == EX G. F Join G = H"
    1.38  
    1.39 -  refines :: ['a program, 'a program, 'a program set] => bool
    1.40 -			("(3_ refines _ wrt _)" [10,10,10] 10)
    1.41 -   "G refines F wrt X ==
    1.42 -      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
    1.43 -
    1.44 -  iso_refines :: ['a program, 'a program, 'a program set] => bool
    1.45 -			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    1.46 -   "G iso_refines F wrt X ==
    1.47 -      F : welldef Int X --> G : welldef Int X"
    1.48 +  strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    1.49  
    1.50  end