src/HOL/UNITY/Comp.thy
 changeset 5612 e981ca6f7332 parent 5597 a12b25c53df1 child 6012 1894bfc4aee9
```     1.1 --- a/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:22:49 1998 +0200
1.2 +++ b/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:27:04 1998 +0200
1.3 @@ -16,24 +16,35 @@
1.4      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
1.5
1.6    ex_prop  :: 'a program set => bool
1.7 -   "ex_prop X == ALL F G. F:X | G: X --> (Join F G) : X"
1.8 +   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
1.9
1.10    strict_ex_prop  :: 'a program set => bool
1.11 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (Join F G : X)"
1.12 +   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
1.13
1.14    uv_prop  :: 'a program set => bool
1.15 -   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (Join F G) : X)"
1.16 +   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (F Join G) : X)"
1.17
1.18    strict_uv_prop  :: 'a program set => bool
1.19 -   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (Join F G : X))"
1.20 +   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
1.21
1.22 -  compatible :: ['a program, 'a program] => bool
1.23 -   "compatible F G == Init F Int Init G ~= {}"
1.24 +  (*Ill-defined programs can arise through "Join"*)
1.25 +  welldef :: 'a program set
1.26 +   "welldef == {F. Init F ~= {}}"
1.27
1.28    component :: ['a program, 'a program] => bool
1.29 -   "component F H == EX G. Join F G = H"
1.30 +   "component F H == EX G. F Join G = H"
1.31
1.32    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
1.33     "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
1.34
1.35 +  refines :: ['a program, 'a program, 'a program set] => bool
1.36 +			("(3_ refines _ wrt _)" [10,10,10] 10)
1.37 +   "G refines F wrt X ==
1.38 +      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
1.39 +
1.40 +  iso_refines :: ['a program, 'a program, 'a program set] => bool
1.41 +			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
1.42 +   "G iso_refines F wrt X ==
1.43 +      F : welldef Int X --> G : welldef Int X"
1.44 +
1.45  end
```