src/HOL/UNITY/Comp.thy

--- a/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:22:49 1998 +0200
+++ b/src/HOL/UNITY/Comp.thy	Mon Oct 05 10:27:04 1998 +0200
@@ -16,24 +16,35 @@
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
   ex_prop  :: 'a program set => bool
-   "ex_prop X == ALL F G. F:X | G: X --> (Join F G) : X"
+   "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
 
   strict_ex_prop  :: 'a program set => bool
-   "strict_ex_prop X == ALL F G. (F:X | G: X) = (Join F G : X)"
+   "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
 
   uv_prop  :: 'a program set => bool
-   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (Join F G) : X)"
+   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (F Join G) : X)"
 
   strict_uv_prop  :: 'a program set => bool
-   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (Join F G : X))"
+   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (F Join G : X))"
 
-  compatible :: ['a program, 'a program] => bool
-   "compatible F G == Init F Int Init G ~= {}"
+  (*Ill-defined programs can arise through "Join"*)
+  welldef :: 'a program set  
+   "welldef == {F. Init F ~= {}}"
 
   component :: ['a program, 'a program] => bool
-   "component F H == EX G. Join F G = H"
+   "component F H == EX G. F Join G = H"
 
   guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
 
+  refines :: ['a program, 'a program, 'a program set] => bool
+			("(3_ refines _ wrt _)" [10,10,10] 10)
+   "G refines F wrt X ==
+      ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
+
+  iso_refines :: ['a program, 'a program, 'a program set] => bool
+			("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
+   "G iso_refines F wrt X ==
+      F : welldef Int X --> G : welldef Int X"
+
 end