17 All_None :: "'a ann_triple_op list \<Rightarrow> bool" |
17 All_None :: "'a ann_triple_op list \<Rightarrow> bool" |
18 "All_None Ts \<equiv> \<forall>(c, q) \<in> set Ts. c = None" |
18 "All_None Ts \<equiv> \<forall>(c, q) \<in> set Ts. c = None" |
19 |
19 |
20 subsection {* The Transition Relation *} |
20 subsection {* The Transition Relation *} |
21 |
21 |
22 consts |
22 inductive_set |
23 ann_transition :: "(('a ann_com_op \<times> 'a) \<times> ('a ann_com_op \<times> 'a)) set" |
23 ann_transition :: "(('a ann_com_op \<times> 'a) \<times> ('a ann_com_op \<times> 'a)) set" |
24 transition :: "(('a com \<times> 'a) \<times> ('a com \<times> 'a)) set" |
24 and transition :: "(('a com \<times> 'a) \<times> ('a com \<times> 'a)) set" |
25 |
25 and ann_transition' :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
26 syntax |
26 ("_ -1\<rightarrow> _"[81,81] 100) |
27 "_ann_transition" :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
27 and transition' :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
28 ("_ -1\<rightarrow> _"[81,81] 100) |
28 ("_ -P1\<rightarrow> _"[81,81] 100) |
29 "_ann_transition_n" :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) |
29 and transitions :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
30 \<Rightarrow> bool" ("_ -_\<rightarrow> _"[81,81] 100) |
30 ("_ -P*\<rightarrow> _"[81,81] 100) |
31 "_ann_transition_*" :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
31 where |
32 ("_ -*\<rightarrow> _"[81,81] 100) |
32 "con_0 -1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition" |
33 |
33 | "con_0 -P1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition" |
34 "_transition" :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" ("_ -P1\<rightarrow> _"[81,81] 100) |
34 | "con_0 -P*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition\<^sup>*" |
35 "_transition_n" :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
35 |
36 ("_ -P_\<rightarrow> _"[81,81,81] 100) |
36 | AnnBasic: "(Some (AnnBasic r f), s) -1\<rightarrow> (None, f s)" |
37 "_transition_*" :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" ("_ -P*\<rightarrow> _"[81,81] 100) |
37 |
|
38 | AnnSeq1: "(Some c0, s) -1\<rightarrow> (None, t) \<Longrightarrow> |
|
39 (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some c1, t)" |
|
40 | AnnSeq2: "(Some c0, s) -1\<rightarrow> (Some c2, t) \<Longrightarrow> |
|
41 (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some (AnnSeq c2 c1), t)" |
|
42 |
|
43 | AnnCond1T: "s \<in> b \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c1, s)" |
|
44 | AnnCond1F: "s \<notin> b \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c2, s)" |
|
45 |
|
46 | AnnCond2T: "s \<in> b \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (Some c, s)" |
|
47 | AnnCond2F: "s \<notin> b \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (None, s)" |
|
48 |
|
49 | AnnWhileF: "s \<notin> b \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow> (None, s)" |
|
50 | AnnWhileT: "s \<in> b \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow> |
|
51 (Some (AnnSeq c (AnnWhile i b i c)), s)" |
|
52 |
|
53 | AnnAwait: "\<lbrakk> s \<in> b; atom_com c; (c, s) -P*\<rightarrow> (Parallel [], t) \<rbrakk> \<Longrightarrow> |
|
54 (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)" |
|
55 |
|
56 | Parallel: "\<lbrakk> i<length Ts; Ts!i = (Some c, q); (Some c, s) -1\<rightarrow> (r, t) \<rbrakk> |
|
57 \<Longrightarrow> (Parallel Ts, s) -P1\<rightarrow> (Parallel (Ts [i:=(r, q)]), t)" |
|
58 |
|
59 | Basic: "(Basic f, s) -P1\<rightarrow> (Parallel [], f s)" |
|
60 |
|
61 | Seq1: "All_None Ts \<Longrightarrow> (Seq (Parallel Ts) c, s) -P1\<rightarrow> (c, s)" |
|
62 | Seq2: "(c0, s) -P1\<rightarrow> (c2, t) \<Longrightarrow> (Seq c0 c1, s) -P1\<rightarrow> (Seq c2 c1, t)" |
|
63 |
|
64 | CondT: "s \<in> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c1, s)" |
|
65 | CondF: "s \<notin> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c2, s)" |
|
66 |
|
67 | WhileF: "s \<notin> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Parallel [], s)" |
|
68 | WhileT: "s \<in> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Seq c (While b i c), s)" |
|
69 |
|
70 monos "rtrancl_mono" |
38 |
71 |
39 text {* The corresponding syntax translations are: *} |
72 text {* The corresponding syntax translations are: *} |
40 |
73 |
41 translations |
74 abbreviation |
42 "con_0 -1\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> ann_transition" |
75 ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) |
43 "con_0 -n\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> ann_transition^n" |
76 \<Rightarrow> bool" ("_ -_\<rightarrow> _"[81,81] 100) where |
44 "con_0 -*\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> ann_transition\<^sup>*" |
77 "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition^n" |
45 |
78 |
46 "con_0 -P1\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> transition" |
79 abbreviation |
47 "con_0 -Pn\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> transition^n" |
80 ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
48 "con_0 -P*\<rightarrow> con_1" \<rightleftharpoons> "(con_0, con_1) \<in> transition\<^sup>*" |
81 ("_ -*\<rightarrow> _"[81,81] 100) where |
49 |
82 "con_0 -*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition\<^sup>*" |
50 inductive ann_transition transition |
83 |
51 intros |
84 abbreviation |
52 AnnBasic: "(Some (AnnBasic r f), s) -1\<rightarrow> (None, f s)" |
85 transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
53 |
86 ("_ -P_\<rightarrow> _"[81,81,81] 100) where |
54 AnnSeq1: "(Some c0, s) -1\<rightarrow> (None, t) \<Longrightarrow> |
87 "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition^n" |
55 (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some c1, t)" |
|
56 AnnSeq2: "(Some c0, s) -1\<rightarrow> (Some c2, t) \<Longrightarrow> |
|
57 (Some (AnnSeq c0 c1), s) -1\<rightarrow> (Some (AnnSeq c2 c1), t)" |
|
58 |
|
59 AnnCond1T: "s \<in> b \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c1, s)" |
|
60 AnnCond1F: "s \<notin> b \<Longrightarrow> (Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> (Some c2, s)" |
|
61 |
|
62 AnnCond2T: "s \<in> b \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (Some c, s)" |
|
63 AnnCond2F: "s \<notin> b \<Longrightarrow> (Some (AnnCond2 r b c), s) -1\<rightarrow> (None, s)" |
|
64 |
|
65 AnnWhileF: "s \<notin> b \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow> (None, s)" |
|
66 AnnWhileT: "s \<in> b \<Longrightarrow> (Some (AnnWhile r b i c), s) -1\<rightarrow> |
|
67 (Some (AnnSeq c (AnnWhile i b i c)), s)" |
|
68 |
|
69 AnnAwait: "\<lbrakk> s \<in> b; atom_com c; (c, s) -P*\<rightarrow> (Parallel [], t) \<rbrakk> \<Longrightarrow> |
|
70 (Some (AnnAwait r b c), s) -1\<rightarrow> (None, t)" |
|
71 |
|
72 Parallel: "\<lbrakk> i<length Ts; Ts!i = (Some c, q); (Some c, s) -1\<rightarrow> (r, t) \<rbrakk> |
|
73 \<Longrightarrow> (Parallel Ts, s) -P1\<rightarrow> (Parallel (Ts [i:=(r, q)]), t)" |
|
74 |
|
75 Basic: "(Basic f, s) -P1\<rightarrow> (Parallel [], f s)" |
|
76 |
|
77 Seq1: "All_None Ts \<Longrightarrow> (Seq (Parallel Ts) c, s) -P1\<rightarrow> (c, s)" |
|
78 Seq2: "(c0, s) -P1\<rightarrow> (c2, t) \<Longrightarrow> (Seq c0 c1, s) -P1\<rightarrow> (Seq c2 c1, t)" |
|
79 |
|
80 CondT: "s \<in> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c1, s)" |
|
81 CondF: "s \<notin> b \<Longrightarrow> (Cond b c1 c2, s) -P1\<rightarrow> (c2, s)" |
|
82 |
|
83 WhileF: "s \<notin> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Parallel [], s)" |
|
84 WhileT: "s \<in> b \<Longrightarrow> (While b i c, s) -P1\<rightarrow> (Seq c (While b i c), s)" |
|
85 |
|
86 monos "rtrancl_mono" |
|
87 |
88 |
88 subsection {* Definition of Semantics *} |
89 subsection {* Definition of Semantics *} |
89 |
90 |
90 constdefs |
91 constdefs |
91 ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" |
92 ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" |