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

crefine: generalise `ccorres_tmp_lift2` 

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Matthew Brecknell 2020-06-27 18:57:53 +10:00 committed by Matthew Brecknell
parent 1dfd9d48dd
commit 337c0d62ea
5 changed files with 8 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
lib/clib/Corres_UL_C.thy
View File

@ -705,19 +705,18 @@ lemmas ceqvhD2 = ceqvhD1 [OF _ _ ceqv_sym]
lemma ccorres_tmp_lift2:
assumes rl: "\<And>t t'. ceqv \<Gamma> xf' rv' t t' c c'"
and c: "ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G'' rv') hs m c'"
and geq: "G'' rv' \<inter> {s. rv' = xf' s} = G' \<inter> {s. rv' = xf' s}"
and geq: "G' \<inter> {s. rv' = xf' s} \<subseteq> G'' rv'"
shows "ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c"
using c
apply -
apply (rule ccorresI')
apply (erule (2) ccorresE)
apply (erule (2) ccorresE)
apply (subst (asm) Int_eq_symmetric)
apply (subst (asm) geq [symmetric])
apply fastforce
apply (drule set_mp[OF geq], clarsimp)
apply assumption
apply simp
apply (erule conjE)+
apply (erule (1) ceqvhD1 [OF _ _ rl])
apply (erule (1) ceqvhD1[OF _ _ rl])
apply simp
apply fastforce
done

2
proof/crefine/ARM/Recycle_C.thy
View File

@ -643,7 +643,7 @@ lemma cancelBadgedSends_ccorres:
apply (induct_tac list)
apply (rule allI)
apply (rule iffD1 [OF ccorres_expand_while_iff_Seq])
apply (rule ccorres_tmp_lift2 [OF _ _ refl])
apply (rule ccorres_tmp_lift2 [OF _ _ Int_lower1])
apply ceqv
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_rhs_assoc2)

2
proof/crefine/ARM_HYP/Recycle_C.thy
View File

@ -983,7 +983,7 @@ lemma cancelBadgedSends_ccorres:
apply (induct_tac list)
apply (rule allI)
apply (rule iffD1 [OF ccorres_expand_while_iff_Seq])
apply (rule ccorres_tmp_lift2 [OF _ _ refl])
apply (rule ccorres_tmp_lift2 [OF _ _ Int_lower1])
apply ceqv
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_rhs_assoc2)

2
proof/crefine/RISCV64/Recycle_C.thy
View File

@ -871,7 +871,7 @@ lemma cancelBadgedSends_ccorres:
apply (induct_tac list)
apply (rule allI)
apply (rule iffD1 [OF ccorres_expand_while_iff_Seq])
apply (rule ccorres_tmp_lift2 [OF _ _ refl])
apply (rule ccorres_tmp_lift2 [OF _ _ Int_lower1])
apply ceqv
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_rhs_assoc2)

2
proof/crefine/X64/Recycle_C.thy
View File

@ -990,7 +990,7 @@ lemma cancelBadgedSends_ccorres:
apply (induct_tac list)
apply (rule allI)
apply (rule iffD1 [OF ccorres_expand_while_iff_Seq])
apply (rule ccorres_tmp_lift2 [OF _ _ refl])
apply (rule ccorres_tmp_lift2 [OF _ _ Int_lower1])
apply ceqv
apply (simp add: ccorres_cond_iffs)
apply (rule ccorres_rhs_assoc2)