src/HOL/UNITY/Guar.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Guar.thy	Tue Aug 31 15:58:38 1999 +0200
@@ -0,0 +1,52 @@
+(*  Title:      HOL/UNITY/Guar.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+Guarantees, etc.
+
+From Chandy and Sanders, "Reasoning About Program Composition"
+*)
+
+Guar = Comp +
+
+instance program :: (term) order
+                    (component_refl, component_trans, component_antisym,
+                     program_less_le)
+
+constdefs
+
+  (*Existential and Universal properties.  I formalize the two-program
+    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 --> (F Join G) : X"
+
+  strict_ex_prop  :: 'a program set => bool
+   "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 --> (F Join G) : X)"
+
+  strict_uv_prop  :: 'a program set => bool
+   "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
+
+  (*Ill-defined programs can arise through "Join"*)
+  welldef :: 'a program set  
+   "welldef == {F. Init F ~= {}}"
+
+  guar :: ['a program set, 'a program set] => 'a program set
+   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
+   "X guarantees Y == {F. ALL H. 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