equal
deleted
inserted
replaced
169 |
169 |
170 lemma AnnAwait_atomics: |
170 lemma AnnAwait_atomics: |
171 "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))" |
171 "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))" |
172 by(simp add: interfree_aux_def oghoare_sound) |
172 by(simp add: interfree_aux_def oghoare_sound) |
173 |
173 |
174 constdefs |
174 definition interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool" where |
175 interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool" |
|
176 "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y) |
175 "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y) |
177 \<and> interfree_aux(com y, post y, com x)" |
176 \<and> interfree_aux(com y, post y, com x)" |
178 |
177 |
179 lemma interfree_swap_Empty: "interfree_swap (x, [])" |
178 lemma interfree_swap_Empty: "interfree_swap (x, [])" |
180 by(simp add:interfree_swap_def) |
179 by(simp add:interfree_swap_def) |
206 lemma interfree_Map: |
205 lemma interfree_Map: |
207 "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j)) |
206 "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j)) |
208 \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])" |
207 \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])" |
209 by(force simp add: interfree_def less_diff_conv) |
208 by(force simp add: interfree_def less_diff_conv) |
210 |
209 |
211 constdefs map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45) |
210 definition map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45) where |
212 "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)" |
211 "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)" |
213 |
212 |
214 lemma MapAnnEmpty: "[\<turnstile>] []" |
213 lemma MapAnnEmpty: "[\<turnstile>] []" |
215 by(simp add:map_ann_hoare_def) |
214 by(simp add:map_ann_hoare_def) |
216 |
215 |