adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle2022 lib: update Concurrency 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2022-11-02 11:24:57 +11:00 committed by Gerwin Klein
parent 821f9ed0c7
commit 7e44994a55
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
lib/concurrency/Atomicity_Lib.thy
View File

@ -60,7 +60,7 @@ lemma interferences_twp[wp]:
(is "\<lbrace>?P\<rbrace>,\<lbrace>R\<rbrace> ?f \<lbrace>G\<rbrace>,\<lbrace>?Q\<rbrace>")
apply (rule validI_strengthen_post, rule repeat_validI)
apply wp
apply (clarsimp simp: reflpD[where r=G])
apply (clarsimp simp: reflpD[where R=G])
apply (metis rtranclp_trans)
apply simp
done
@ -470,7 +470,7 @@ lemma rel_tr_refinement_bind_left_general:
apply (simp add: image_def)
apply (strengthen bexI[mk_strg I _ E] | simp)+
apply (simp add: list_all2_append rely_cond_append
list_all2_same reflpD[where r=sr] rel_prod_sel
list_all2_same reflpD[where R=sr] rel_prod_sel
split del: if_split)
apply (erule rely_cond_equiv_s)
apply (erule disjE)
@ -493,7 +493,7 @@ lemma rel_tr_refinement_bind_right_general:
apply (erule elem_bindE)
apply (clarsimp simp: bind_def)
apply (strengthen bexI[mk_strg I _ E], simp)
apply (auto simp: list_all2_same reflpD[where r=sr])[1]
apply (auto simp: list_all2_same reflpD[where R=sr])[1]
apply (clarsimp simp: rely_cond_append)
apply (drule validI_D, erule(1) conjI, assumption+, clarsimp)
apply (drule spec, drule(3) rel_tr_refinementD,
@ -502,7 +502,7 @@ lemma rel_tr_refinement_bind_right_general:
apply (simp add: image_def)
apply (strengthen bexI[mk_strg I _ E] | simp)+
apply (simp add: list_all2_append list_all2_lengthD)
apply (simp add: rely_cond_append list_all2_same reflpD[where r=sr] rel_prod_sel
apply (simp add: rely_cond_append list_all2_same reflpD[where R=sr] rel_prod_sel
split del: if_split)
done