--- a/src/HOL/UNITY/Union.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Union.thy Mon Oct 18 15:18:24 1999 +0200
@@ -22,17 +22,25 @@
SKIP :: 'a program
"SKIP == mk_program (UNIV, {})"
- Diff :: "['a program, ('a * 'a)set set] => 'a program"
- "Diff F acts == mk_program (Init F, Acts F - acts)"
+ Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
+ "Diff C G acts ==
+ mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
(*The set of systems that regard "v" as local to F*)
- localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
- "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
+ LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
+ ("(_/ localTo[_]/ _)" [80,0,80] 80)
+ "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
+
+ (*The weak version of localTo, considering only G's reachable states*)
+ LocalTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
+ "v LocalTo F == {G. G : v localTo[reachable G] F}"
(*Two programs with disjoint actions, except for identity actions.
It's a weak property but still useful.*)
- Disjoint :: ['a program, 'a program] => bool
- "Disjoint F G == Acts F Int Acts G <= {Id}"
+ Disjoint :: ['a set, 'a program, 'a program] => bool
+ "Disjoint C F G ==
+ (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
+ <= {}"
syntax
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)