src/HOL/UNITY/Union.thy
changeset 7878 43b03d412b82
parent 7826 c6a8b73b6c2a
child 7915 c7fd7eb3b0ef
     1.1 --- a/src/HOL/UNITY/Union.thy	Mon Oct 18 15:17:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Mon Oct 18 15:18:24 1999 +0200
     1.3 @@ -22,17 +22,25 @@
     1.4    SKIP :: 'a program
     1.5      "SKIP == mk_program (UNIV, {})"
     1.6  
     1.7 -  Diff :: "['a program, ('a * 'a)set set] => 'a program"
     1.8 -    "Diff F acts == mk_program (Init F, Acts F - acts)"
     1.9 +  Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
    1.10 +    "Diff C G acts ==
    1.11 +       mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
    1.12  
    1.13    (*The set of systems that regard "v" as local to F*)
    1.14 -  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    1.15 -    "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
    1.16 +  LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
    1.17 +                                           ("(_/ localTo[_]/ _)" [80,0,80] 80)
    1.18 +    "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
    1.19 +
    1.20 +  (*The weak version of localTo, considering only G's reachable states*)
    1.21 +  LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
    1.22 +    "v LocalTo F == {G. G : v localTo[reachable G] F}"
    1.23  
    1.24    (*Two programs with disjoint actions, except for identity actions.
    1.25      It's a weak property but still useful.*)
    1.26 -  Disjoint :: ['a program, 'a program] => bool
    1.27 -    "Disjoint F G == Acts F Int Acts G <= {Id}"
    1.28 +  Disjoint :: ['a set, 'a program, 'a program] => bool
    1.29 +    "Disjoint C F G ==
    1.30 +       (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
    1.31 +       <= {}"
    1.32  
    1.33  syntax
    1.34    "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)