src/HOL/UNITY/Comp.thy
 changeset 6012 1894bfc4aee9 parent 5612 e981ca6f7332 child 6138 b7e6e607bb4d
```     1.1 --- a/src/HOL/UNITY/Comp.thy	Wed Dec 02 16:14:09 1998 +0100
1.2 +++ b/src/HOL/UNITY/Comp.thy	Thu Dec 03 10:45:06 1998 +0100
1.3 @@ -16,23 +16,29 @@
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 --> (F Join G) : X"
1.8 +   "ex_prop X ==
1.9 +      ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
1.10
1.11    strict_ex_prop  :: 'a program set => bool
1.12 -   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
1.13 +   "strict_ex_prop X ==
1.14 +      ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
1.15
1.16    uv_prop  :: 'a program set => bool
1.17 -   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (F Join G) : X)"
1.18 +   "uv_prop X ==
1.19 +      SKIP UNIV : X &
1.20 +      (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
1.21
1.22    strict_uv_prop  :: 'a program set => bool
1.23 -   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
1.24 +   "strict_uv_prop X ==
1.25 +      SKIP UNIV : X &
1.26 +      (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
1.27
1.28    (*Ill-defined programs can arise through "Join"*)
1.29    welldef :: 'a program set
1.30     "welldef == {F. Init F ~= {}}"
1.31
1.32    component :: ['a program, 'a program] => bool
1.33 -   "component F H == EX G. F Join G = H"
1.34 +   "component F H == EX G. F Join G = H & States F = States G"
1.35
1.36    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
1.37     "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
1.38 @@ -40,7 +46,9 @@
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 +      States F = States G &
1.44 +      (ALL H. States F = States H & (F Join H) : welldef Int X
1.45 +        --> G Join H : welldef Int X)"
1.46
1.47    iso_refines :: ['a program, 'a program, 'a program set] => bool
1.48  			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
```