--- a/src/HOL/UNITY/Union.thy Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Union.thy Sat Sep 23 16:02:01 2000 +0200
@@ -11,14 +11,30 @@
Union = SubstAx + FP +
constdefs
+
+ (*FIXME: conjoin Init F Int Init G ~= {} *)
+ ok :: ['a program, 'a program] => bool (infixl 65)
+ "F ok G == Acts F <= AllowedActs G &
+ Acts G <= AllowedActs F"
+
+ (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *)
+ OK :: ['a set, 'a => 'b program] => bool
+ "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
+
JOIN :: ['a set, 'a => 'b program] => 'b program
- "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
+ "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
+ INT i:I. AllowedActs (F i))"
Join :: ['a program, 'a program] => 'a program (infixl 65)
- "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
+ "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
+ AllowedActs F Int AllowedActs G)"
SKIP :: 'a program
- "SKIP == mk_program (UNIV, {})"
+ "SKIP == mk_program (UNIV, {}, UNIV)"
+
+ (*Characterizes safety properties. Used with specifying AllowedActs*)
+ safety_prop :: "'a program set => bool"
+ "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
syntax
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)