From abca2deeab4c8890a6f631b3c2cf8cadb30d7a6e Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 21 Feb 2025 15:48:56 +1030 Subject: [PATCH] lib: add gets_gets_the_corres_ex_abs' to ExtraCorres Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index 93e70969ec..f5c4de47cb 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -379,12 +379,22 @@ lemmas corres_symb_exec_r_conj_ex_abs_forwards = corres_symb_exec_r_conj_ex_abs[where P=P and Q=P for P, where P'=P' and Q'=P' for P', simplified] lemma gets_the_corres_ex_abs': - "\no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\ \ + "\no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\ \ corres_underlying sr False True r P P' (gets_the a) (gets_the b) = (\s s'. P s \ P' s' \ (s, s') \ sr \ r (the (a s)) (the (b s')))" by (fastforce simp: gets_the_def no_ofail_def corres_underlying_def split_def exec_gets assert_opt_def fail_def return_def ex_abs_underlying_def) +lemma gets_gets_the_corres_ex_abs': + "no_ofail (P' and ex_abs_underlying sr P) b \ + corres_underlying sr False True r P P' (gets a) (gets_the b) + = (\s s'. P s \ P' s' \ (s, s') \ sr \ r ((a s)) (the (b s')))" + apply (frule gets_the_corres_ex_abs'[where a="ogets a" and r=r, rotated]) + apply wpsimp + apply (clarsimp simp: gets_the_ogets) + apply (clarsimp simp: ogets_def) + done + lemmas gets_the_corres_ex_abs = gets_the_corres_ex_abs'[THEN iffD2] lemma gets_the_corres':