13 theory Union imports SubstAx FP |
13 theory Union imports SubstAx FP |
14 begin |
14 begin |
15 |
15 |
16 definition |
16 definition |
17 (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *) |
17 (*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *) |
18 ok :: "[i, i] => o" (infixl "ok" 65) where |
18 ok :: "[i, i] => o" (infixl \<open>ok\<close> 65) where |
19 "F ok G == Acts(F) \<subseteq> AllowedActs(G) & |
19 "F ok G == Acts(F) \<subseteq> AllowedActs(G) & |
20 Acts(G) \<subseteq> AllowedActs(F)" |
20 Acts(G) \<subseteq> AllowedActs(F)" |
21 |
21 |
22 definition |
22 definition |
23 (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *) |
23 (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *) |
29 "JOIN(I,F) == if I = 0 then SKIP else |
29 "JOIN(I,F) == if I = 0 then SKIP else |
30 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)), |
30 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)), |
31 \<Inter>i \<in> I. AllowedActs(F(i)))" |
31 \<Inter>i \<in> I. AllowedActs(F(i)))" |
32 |
32 |
33 definition |
33 definition |
34 Join :: "[i, i] => i" (infixl "\<squnion>" 65) where |
34 Join :: "[i, i] => i" (infixl \<open>\<squnion>\<close> 65) where |
35 "F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G), |
35 "F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G), |
36 AllowedActs(F) \<inter> AllowedActs(G))" |
36 AllowedActs(F) \<inter> AllowedActs(G))" |
37 definition |
37 definition |
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)) \<longrightarrow> G \<in> X)" |
41 SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)" |
42 |
42 |
43 syntax |
43 syntax |
44 "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion>_./ _)" 10) |
44 "_JOIN1" :: "[pttrns, i] => i" (\<open>(3\<Squnion>_./ _)\<close> 10) |
45 "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion>_ \<in> _./ _)" 10) |
45 "_JOIN" :: "[pttrn, i, i] => i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10) |
46 |
46 |
47 translations |
47 translations |
48 "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))" |
48 "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))" |
49 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" |
49 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" |
50 "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))" |
50 "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))" |