33 |
33 |
34 (*Characterizes safety properties. Used with specifying Allowed*) |
34 (*Characterizes safety properties. Used with specifying Allowed*) |
35 safety_prop :: "'a program set => bool" |
35 safety_prop :: "'a program set => bool" |
36 "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)" |
36 "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)" |
37 |
37 |
|
38 notation |
|
39 SKIP ("\<bottom>") and |
|
40 Join (infixl "\<squnion>" 65) |
|
41 |
38 syntax |
42 syntax |
39 "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) |
43 "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) |
40 "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) |
44 "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) |
|
45 syntax (xsymbols) |
|
46 "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) |
|
47 "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10) |
41 |
48 |
42 translations |
49 translations |
43 "JN x: A. B" == "CONST JOIN A (%x. B)" |
50 "JN x: A. B" == "CONST JOIN A (%x. B)" |
44 "JN x y. B" == "JN x. JN y. B" |
51 "JN x y. B" == "JN x. JN y. B" |
45 "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)" |
52 "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)" |
46 |
|
47 syntax (xsymbols) |
|
48 SKIP :: "'a program" ("\<bottom>") |
|
49 Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) |
|
50 "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) |
|
51 "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10) |
|
52 |
53 |
53 |
54 |
54 subsection{*SKIP*} |
55 subsection{*SKIP*} |
55 |
56 |
56 lemma Init_SKIP [simp]: "Init SKIP = UNIV" |
57 lemma Init_SKIP [simp]: "Init SKIP = UNIV" |