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

clib: move ccorresG abbreviation 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2023-01-30 11:47:24 +10:30 committed by michaelmcinerney
parent c257b46009
commit 2119182166
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/clib/CCorresLemmas.thy
View File

@ -345,9 +345,6 @@ lemma ccorres_expand_while_iff:
apply (auto elim!: exec_Normal_elim_cases intro: exec.intros)
done
abbreviation
"ccorresG rf_sr \<Gamma> r xf \<equiv> ccorres_underlying rf_sr \<Gamma> r xf r xf"
lemma exec_handlers_Hoare_call_Basic:
"\<lbrakk> \<forall>s' t x. s' \<in> P \<longrightarrow> g s' t (ret s' t) \<in> Q; UNIV \<subseteq> A \<rbrakk> \<Longrightarrow>
exec_handlers_Hoare \<Gamma> P (call initfn p ret (\<lambda>x y. Basic (g x y)) # hs) Q A"

3
lib/clib/Corres_UL_C.thy
View File

@ -86,6 +86,9 @@ where
\<and> unif_rrel (n = length hs) rrel xf arrel axf r s'')
| _ \<Rightarrow> False))"
abbreviation
"ccorresG rf_sr \<Gamma> r xf \<equiv> ccorres_underlying rf_sr \<Gamma> r xf r xf"
declare isNormal_simps [simp]
lemma ccorresI [case_names fail nofail]: