src/HOL/UNITY/Comp.thy
 changeset 6295 351b3c2b0d83 parent 6138 b7e6e607bb4d child 6646 3ea726909fff
```     1.1 --- a/src/HOL/UNITY/Comp.thy	Mon Mar 01 18:37:52 1999 +0100
1.2 +++ b/src/HOL/UNITY/Comp.thy	Mon Mar 01 18:38:43 1999 +0100
1.3 @@ -6,11 +6,6 @@
1.4  Composition
1.5
1.6  From Chandy and Sanders, "Reasoning About Program Composition"
1.7 -
1.8 -QUESTIONS:
1.9 -  refines_def: needs the States F = States G?
1.10 -
1.11 -  uv_prop, component: should be States F = States (F Join G)
1.12  *)
1.13
1.14  Comp = Union +
1.15 @@ -21,29 +16,23 @@
1.16      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
1.17
1.18    ex_prop  :: 'a program set => bool
1.19 -   "ex_prop X ==
1.20 -      ALL F G. (F:X | G: X) & States F = States G --> (F Join G) : X"
1.21 +   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
1.22
1.23    strict_ex_prop  :: 'a program set => bool
1.24 -   "strict_ex_prop X ==
1.25 -      ALL F G. States F = States G --> (F:X | G: X) = (F Join G : X)"
1.26 +   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
1.27
1.28    uv_prop  :: 'a program set => bool
1.29 -   "uv_prop X ==
1.30 -      SKIP UNIV : X &
1.31 -      (ALL F G. F:X & G: X & States F = States G --> (F Join G) : X)"
1.32 +   "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
1.33
1.34    strict_uv_prop  :: 'a program set => bool
1.35 -   "strict_uv_prop X ==
1.36 -      SKIP UNIV : X &
1.37 -      (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))"
1.38 +   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
1.39
1.40    (*Ill-defined programs can arise through "Join"*)
1.41    welldef :: 'a program set
1.42     "welldef == {F. Init F ~= {}}"
1.43
1.44    component :: ['a program, 'a program] => bool
1.45 -   "component F H == EX G. F Join G = H & States F = States G"
1.46 +   "component F H == EX G. F Join G = H"
1.47
1.48    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
1.49     "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
1.50 @@ -51,9 +40,7 @@
1.51    refines :: ['a program, 'a program, 'a program set] => bool
1.52  			("(3_ refines _ wrt _)" [10,10,10] 10)
1.53     "G refines F wrt X ==
1.54 -      States F = States G &
1.55 -      (ALL H. States F = States H & (F Join H) : welldef Int X
1.56 -        --> G Join H : welldef Int X)"
1.57 +      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
1.58
1.59    iso_refines :: ['a program, 'a program, 'a program set] => bool
1.60  			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
```