38 (*Characterizes safety properties. Used with specifying AllowedActs*) |
38 (*Characterizes safety properties. Used with specifying AllowedActs*) |
39 safety_prop :: "i => o" where |
39 safety_prop :: "i => o" where |
40 "safety_prop(X) == X\<subseteq>program & |
40 "safety_prop(X) == X\<subseteq>program & |
41 SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)" |
41 SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)" |
42 |
42 |
|
43 notation (xsymbols) |
|
44 SKIP ("\<bottom>") and |
|
45 Join (infixl "\<squnion>" 65) |
|
46 |
43 syntax |
47 syntax |
44 "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) |
48 "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) |
45 "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) |
49 "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) |
|
50 syntax (xsymbols) |
|
51 "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10) |
|
52 "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10) |
46 |
53 |
47 translations |
54 translations |
48 "JN x:A. B" == "CONST JOIN(A, (%x. B))" |
55 "JN x:A. B" == "CONST JOIN(A, (%x. B))" |
49 "JN x y. B" == "JN x. JN y. B" |
56 "JN x y. B" == "JN x. JN y. B" |
50 "JN x. B" == "CONST JOIN(CONST state,(%x. B))" |
57 "JN x. B" == "CONST JOIN(CONST state,(%x. B))" |
51 |
|
52 notation (xsymbols) |
|
53 SKIP ("\<bottom>") and |
|
54 Join (infixl "\<squnion>" 65) |
|
55 |
|
56 syntax (xsymbols) |
|
57 "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10) |
|
58 "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10) |
|
59 |
58 |
60 |
59 |
61 subsection{*SKIP*} |
60 subsection{*SKIP*} |
62 |
61 |
63 lemma reachable_SKIP [simp]: "reachable(SKIP) = state" |
62 lemma reachable_SKIP [simp]: "reachable(SKIP) = state" |