clib: add ccorresE_gets_the rule
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
parent
3573111a7c
commit
7bf5798c0b
|
@ -14,6 +14,7 @@ imports
|
|||
CParser.LemmaBucket_C
|
||||
Lib.LemmaBucket
|
||||
SIMPL_Lemmas
|
||||
Monads.OptionMonadWP
|
||||
begin
|
||||
|
||||
declare word_neq_0_conv [simp del]
|
||||
|
@ -171,6 +172,13 @@ lemma ccorresE:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma ccorresE_gets_the:
|
||||
"\<lbrakk>ccorresG srel \<Gamma> rrel xf G G' hs (gets_the c) c'; (s, s') \<in> srel; G s; s' \<in> G'; no_ofail G c;
|
||||
\<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs, s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk>
|
||||
\<Longrightarrow> (s, t') \<in> srel \<and> rrel (the (c s)) (xf t')"
|
||||
by (fastforce simp: ccorres_underlying_def no_ofail_def unif_rrel_def gets_the_def gets_def
|
||||
get_def bind_def return_def)
|
||||
|
||||
lemma ccorres_empty_handler_abrupt:
|
||||
assumes cc: "ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c"
|
||||
and asms: "(s, s') \<in> sr" "P s" "s' \<in> P'" "\<not> snd (a s)"
|
||||
|
|
Loading…
Reference in New Issue