1 |
|
2 header {* \section{Operational Semantics} *} |
|
3 |
|
4 theory OG_Tran imports OG_Com begin |
|
5 |
|
6 types |
|
7 'a ann_com_op = "('a ann_com) option" |
|
8 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)" |
|
9 |
|
10 consts com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" |
|
11 primrec "com (c, q) = c" |
|
12 |
|
13 consts post :: "'a ann_triple_op \<Rightarrow> 'a assn" |
|
14 primrec "post (c, q) = q" |
|
15 |
|
16 constdefs |
|
17 All_None :: "'a ann_triple_op list \<Rightarrow> bool" |
|
18 "All_None Ts \<equiv> \<forall>(c, q) \<in> set Ts. c = None" |
|
19 |
|
20 subsection {* The Transition Relation *} |
|
21 |
|
22 inductive_set |
|
23 ann_transition :: "(('a ann_com_op \<times> 'a) \<times> ('a ann_com_op \<times> 'a)) set" |
|
24 and transition :: "(('a com \<times> 'a) \<times> ('a com \<times> 'a)) set" |
|
25 and ann_transition' :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
|
26 ("_ -1\<rightarrow> _"[81,81] 100) |
|
27 and transition' :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
|
28 ("_ -P1\<rightarrow> _"[81,81] 100) |
|
29 and transitions :: "('a com \<times> 'a) \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
|
30 ("_ -P*\<rightarrow> _"[81,81] 100) |
|
31 where |
|
32 "con_0 -1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition" |
|
33 | "con_0 -P1\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition" |
|
34 | "con_0 -P*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition\<^sup>*" |
|
35 |
|
36 | AnnBasic: "(Some (AnnBasic r f), s) -1\<rightarrow> (None, f s)" |
|
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" |
|
71 |
|
72 text {* The corresponding syntax translations are: *} |
|
73 |
|
74 abbreviation |
|
75 ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) |
|
76 \<Rightarrow> bool" ("_ -_\<rightarrow> _"[81,81] 100) where |
|
77 "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n" |
|
78 |
|
79 abbreviation |
|
80 ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool" |
|
81 ("_ -*\<rightarrow> _"[81,81] 100) where |
|
82 "con_0 -*\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition\<^sup>*" |
|
83 |
|
84 abbreviation |
|
85 transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool" |
|
86 ("_ -P_\<rightarrow> _"[81,81,81] 100) where |
|
87 "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n" |
|
88 |
|
89 subsection {* Definition of Semantics *} |
|
90 |
|
91 constdefs |
|
92 ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
93 "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}" |
|
94 |
|
95 ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
96 "ann_SEM c S \<equiv> \<Union>ann_sem c ` S" |
|
97 |
|
98 sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" |
|
99 "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}" |
|
100 |
|
101 SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
102 "SEM c S \<equiv> \<Union>sem c ` S " |
|
103 |
|
104 syntax "_Omega" :: "'a com" ("\<Omega>" 63) |
|
105 translations "\<Omega>" \<rightleftharpoons> "While CONST UNIV CONST UNIV (Basic id)" |
|
106 |
|
107 consts fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com" |
|
108 primrec |
|
109 "fwhile b c 0 = \<Omega>" |
|
110 "fwhile b c (Suc n) = Cond b (Seq c (fwhile b c n)) (Basic id)" |
|
111 |
|
112 subsubsection {* Proofs *} |
|
113 |
|
114 declare ann_transition_transition.intros [intro] |
|
115 inductive_cases transition_cases: |
|
116 "(Parallel T,s) -P1\<rightarrow> t" |
|
117 "(Basic f, s) -P1\<rightarrow> t" |
|
118 "(Seq c1 c2, s) -P1\<rightarrow> t" |
|
119 "(Cond b c1 c2, s) -P1\<rightarrow> t" |
|
120 "(While b i c, s) -P1\<rightarrow> t" |
|
121 |
|
122 lemma Parallel_empty_lemma [rule_format (no_asm)]: |
|
123 "(Parallel [],s) -Pn\<rightarrow> (Parallel Ts,t) \<longrightarrow> Ts=[] \<and> n=0 \<and> s=t" |
|
124 apply(induct n) |
|
125 apply(simp (no_asm)) |
|
126 apply clarify |
|
127 apply(drule rel_pow_Suc_D2) |
|
128 apply(force elim:transition_cases) |
|
129 done |
|
130 |
|
131 lemma Parallel_AllNone_lemma [rule_format (no_asm)]: |
|
132 "All_None Ss \<longrightarrow> (Parallel Ss,s) -Pn\<rightarrow> (Parallel Ts,t) \<longrightarrow> Ts=Ss \<and> n=0 \<and> s=t" |
|
133 apply(induct "n") |
|
134 apply(simp (no_asm)) |
|
135 apply clarify |
|
136 apply(drule rel_pow_Suc_D2) |
|
137 apply clarify |
|
138 apply(erule transition_cases,simp_all) |
|
139 apply(force dest:nth_mem simp add:All_None_def) |
|
140 done |
|
141 |
|
142 lemma Parallel_AllNone: "All_None Ts \<Longrightarrow> (SEM (Parallel Ts) X) = X" |
|
143 apply (unfold SEM_def sem_def) |
|
144 apply auto |
|
145 apply(drule rtrancl_imp_UN_rel_pow) |
|
146 apply clarify |
|
147 apply(drule Parallel_AllNone_lemma) |
|
148 apply auto |
|
149 done |
|
150 |
|
151 lemma Parallel_empty: "Ts=[] \<Longrightarrow> (SEM (Parallel Ts) X) = X" |
|
152 apply(rule Parallel_AllNone) |
|
153 apply(simp add:All_None_def) |
|
154 done |
|
155 |
|
156 text {* Set of lemmas from Apt and Olderog "Verification of sequential |
|
157 and concurrent programs", page 63. *} |
|
158 |
|
159 lemma L3_5i: "X\<subseteq>Y \<Longrightarrow> SEM c X \<subseteq> SEM c Y" |
|
160 apply (unfold SEM_def) |
|
161 apply force |
|
162 done |
|
163 |
|
164 lemma L3_5ii_lemma1: |
|
165 "\<lbrakk> (c1, s1) -P*\<rightarrow> (Parallel Ts, s2); All_None Ts; |
|
166 (c2, s2) -P*\<rightarrow> (Parallel Ss, s3); All_None Ss \<rbrakk> |
|
167 \<Longrightarrow> (Seq c1 c2, s1) -P*\<rightarrow> (Parallel Ss, s3)" |
|
168 apply(erule converse_rtrancl_induct2) |
|
169 apply(force intro:converse_rtrancl_into_rtrancl)+ |
|
170 done |
|
171 |
|
172 lemma L3_5ii_lemma2 [rule_format (no_asm)]: |
|
173 "\<forall>c1 c2 s t. (Seq c1 c2, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> |
|
174 (All_None Ts) \<longrightarrow> (\<exists>y m Rs. (c1,s) -P*\<rightarrow> (Parallel Rs, y) \<and> |
|
175 (All_None Rs) \<and> (c2, y) -Pm\<rightarrow> (Parallel Ts, t) \<and> m \<le> n)" |
|
176 apply(induct "n") |
|
177 apply(force) |
|
178 apply(safe dest!: rel_pow_Suc_D2) |
|
179 apply(erule transition_cases,simp_all) |
|
180 apply (fast intro!: le_SucI) |
|
181 apply (fast intro!: le_SucI elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl) |
|
182 done |
|
183 |
|
184 lemma L3_5ii_lemma3: |
|
185 "\<lbrakk>(Seq c1 c2,s) -P*\<rightarrow> (Parallel Ts,t); All_None Ts\<rbrakk> \<Longrightarrow> |
|
186 (\<exists>y Rs. (c1,s) -P*\<rightarrow> (Parallel Rs,y) \<and> All_None Rs |
|
187 \<and> (c2,y) -P*\<rightarrow> (Parallel Ts,t))" |
|
188 apply(drule rtrancl_imp_UN_rel_pow) |
|
189 apply(fast dest: L3_5ii_lemma2 rel_pow_imp_rtrancl) |
|
190 done |
|
191 |
|
192 lemma L3_5ii: "SEM (Seq c1 c2) X = SEM c2 (SEM c1 X)" |
|
193 apply (unfold SEM_def sem_def) |
|
194 apply auto |
|
195 apply(fast dest: L3_5ii_lemma3) |
|
196 apply(fast elim: L3_5ii_lemma1) |
|
197 done |
|
198 |
|
199 lemma L3_5iii: "SEM (Seq (Seq c1 c2) c3) X = SEM (Seq c1 (Seq c2 c3)) X" |
|
200 apply (simp (no_asm) add: L3_5ii) |
|
201 done |
|
202 |
|
203 lemma L3_5iv: |
|
204 "SEM (Cond b c1 c2) X = (SEM c1 (X \<inter> b)) Un (SEM c2 (X \<inter> (-b)))" |
|
205 apply (unfold SEM_def sem_def) |
|
206 apply auto |
|
207 apply(erule converse_rtranclE) |
|
208 prefer 2 |
|
209 apply (erule transition_cases,simp_all) |
|
210 apply(fast intro: converse_rtrancl_into_rtrancl elim: transition_cases)+ |
|
211 done |
|
212 |
|
213 |
|
214 lemma L3_5v_lemma1[rule_format]: |
|
215 "(S,s) -Pn\<rightarrow> (T,t) \<longrightarrow> S=\<Omega> \<longrightarrow> (\<not>(\<exists>Rs. T=(Parallel Rs) \<and> All_None Rs))" |
|
216 apply (unfold UNIV_def) |
|
217 apply(rule nat_less_induct) |
|
218 apply safe |
|
219 apply(erule rel_pow_E2) |
|
220 apply simp_all |
|
221 apply(erule transition_cases) |
|
222 apply simp_all |
|
223 apply(erule rel_pow_E2) |
|
224 apply(simp add: Id_def) |
|
225 apply(erule transition_cases,simp_all) |
|
226 apply clarify |
|
227 apply(erule transition_cases,simp_all) |
|
228 apply(erule rel_pow_E2,simp) |
|
229 apply clarify |
|
230 apply(erule transition_cases) |
|
231 apply simp+ |
|
232 apply clarify |
|
233 apply(erule transition_cases) |
|
234 apply simp_all |
|
235 done |
|
236 |
|
237 lemma L3_5v_lemma2: "\<lbrakk>(\<Omega>, s) -P*\<rightarrow> (Parallel Ts, t); All_None Ts \<rbrakk> \<Longrightarrow> False" |
|
238 apply(fast dest: rtrancl_imp_UN_rel_pow L3_5v_lemma1) |
|
239 done |
|
240 |
|
241 lemma L3_5v_lemma3: "SEM (\<Omega>) S = {}" |
|
242 apply (unfold SEM_def sem_def) |
|
243 apply(fast dest: L3_5v_lemma2) |
|
244 done |
|
245 |
|
246 lemma L3_5v_lemma4 [rule_format]: |
|
247 "\<forall>s. (While b i c, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> |
|
248 (\<exists>k. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t))" |
|
249 apply(rule nat_less_induct) |
|
250 apply safe |
|
251 apply(erule rel_pow_E2) |
|
252 apply safe |
|
253 apply(erule transition_cases,simp_all) |
|
254 apply (rule_tac x = "1" in exI) |
|
255 apply(force dest: Parallel_empty_lemma intro: converse_rtrancl_into_rtrancl simp add: Id_def) |
|
256 apply safe |
|
257 apply(drule L3_5ii_lemma2) |
|
258 apply safe |
|
259 apply(drule le_imp_less_Suc) |
|
260 apply (erule allE , erule impE,assumption) |
|
261 apply (erule allE , erule impE, assumption) |
|
262 apply safe |
|
263 apply (rule_tac x = "k+1" in exI) |
|
264 apply(simp (no_asm)) |
|
265 apply(rule converse_rtrancl_into_rtrancl) |
|
266 apply fast |
|
267 apply(fast elim: L3_5ii_lemma1) |
|
268 done |
|
269 |
|
270 lemma L3_5v_lemma5 [rule_format]: |
|
271 "\<forall>s. (fwhile b c k, s) -P*\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> |
|
272 (While b i c, s) -P*\<rightarrow> (Parallel Ts,t)" |
|
273 apply(induct "k") |
|
274 apply(force dest: L3_5v_lemma2) |
|
275 apply safe |
|
276 apply(erule converse_rtranclE) |
|
277 apply simp_all |
|
278 apply(erule transition_cases,simp_all) |
|
279 apply(rule converse_rtrancl_into_rtrancl) |
|
280 apply(fast) |
|
281 apply(fast elim!: L3_5ii_lemma1 dest: L3_5ii_lemma3) |
|
282 apply(drule rtrancl_imp_UN_rel_pow) |
|
283 apply clarify |
|
284 apply(erule rel_pow_E2) |
|
285 apply simp_all |
|
286 apply(erule transition_cases,simp_all) |
|
287 apply(fast dest: Parallel_empty_lemma) |
|
288 done |
|
289 |
|
290 lemma L3_5v: "SEM (While b i c) = (\<lambda>x. (\<Union>k. SEM (fwhile b c k) x))" |
|
291 apply(rule ext) |
|
292 apply (simp add: SEM_def sem_def) |
|
293 apply safe |
|
294 apply(drule rtrancl_imp_UN_rel_pow,simp) |
|
295 apply clarify |
|
296 apply(fast dest:L3_5v_lemma4) |
|
297 apply(fast intro: L3_5v_lemma5) |
|
298 done |
|
299 |
|
300 section {* Validity of Correctness Formulas *} |
|
301 |
|
302 constdefs |
|
303 com_validity :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool" ("(3\<parallel>= _// _//_)" [90,55,90] 50) |
|
304 "\<parallel>= p c q \<equiv> SEM c p \<subseteq> q" |
|
305 |
|
306 ann_com_validity :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool" ("\<Turnstile> _ _" [60,90] 45) |
|
307 "\<Turnstile> c q \<equiv> ann_SEM c (pre c) \<subseteq> q" |
|
308 |
|
309 end |
|