src/HOL/UNITY/Union.thy
changeset 10064 1a77667b21ef
parent 9685 6d123a7e30bd
child 12114 a8e860c86252
     1.1 --- a/src/HOL/UNITY/Union.thy	Fri Sep 22 17:25:09 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Sat Sep 23 16:02:01 2000 +0200
     1.3 @@ -11,14 +11,30 @@
     1.4  Union = SubstAx + FP +
     1.5  
     1.6  constdefs
     1.7 +
     1.8 +  (*FIXME: conjoin Init F Int Init G ~= {} *) 
     1.9 +  ok :: ['a program, 'a program] => bool      (infixl 65)
    1.10 +    "F ok G == Acts F <= AllowedActs G &
    1.11 +               Acts G <= AllowedActs F"
    1.12 +
    1.13 +  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
    1.14 +  OK  :: ['a set, 'a => 'b program] => bool
    1.15 +    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
    1.16 +
    1.17    JOIN  :: ['a set, 'a => 'b program] => 'b program
    1.18 -    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
    1.19 +    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
    1.20 +			     INT i:I. AllowedActs (F i))"
    1.21  
    1.22    Join :: ['a program, 'a program] => 'a program      (infixl 65)
    1.23 -    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
    1.24 +    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
    1.25 +			     AllowedActs F Int AllowedActs G)"
    1.26  
    1.27    SKIP :: 'a program
    1.28 -    "SKIP == mk_program (UNIV, {})"
    1.29 +    "SKIP == mk_program (UNIV, {}, UNIV)"
    1.30 +
    1.31 +  (*Characterizes safety properties.  Used with specifying AllowedActs*)
    1.32 +  safety_prop :: "'a program set => bool"
    1.33 +    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
    1.34  
    1.35  syntax
    1.36    "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)