equal
deleted
inserted
replaced
41 SKIP \<in> X \<and> (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)" |
41 SKIP \<in> X \<and> (\<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] \<Rightarrow> i" (\<open>(3\<Squnion>_./ _)\<close> 10) |
44 "_JOIN1" :: "[pttrns, i] \<Rightarrow> i" (\<open>(3\<Squnion>_./ _)\<close> 10) |
45 "_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10) |
45 "_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10) |
|
46 syntax_consts |
|
47 "_JOIN1" "_JOIN" == JOIN |
46 translations |
48 translations |
47 "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))" |
49 "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))" |
48 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" |
50 "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B" |
49 "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))" |
51 "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))" |
50 syntax_consts |
|
51 "_JOIN1" "_JOIN" == JOIN |
|
52 |
52 |
53 |
53 |
54 subsection\<open>SKIP\<close> |
54 subsection\<open>SKIP\<close> |
55 |
55 |
56 lemma reachable_SKIP [simp]: "reachable(SKIP) = state" |
56 lemma reachable_SKIP [simp]: "reachable(SKIP) = state" |