From 4b8866e3813d3d22b9ec86fab6de3b1be43ca89c Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Fri, 12 Jan 2024 18:45:17 +1030
Subject: [PATCH] lib: add gets_the_corres, make lemmas statements, fix
 indentation squash

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/ExtraCorres.thy | 32 ++++++++++++++++++++++----------
 1 file changed, 22 insertions(+), 10 deletions(-)

diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy
index 91fab85e2c..eed9d65d34 100644
--- a/lib/ExtraCorres.thy
+++ b/lib/ExtraCorres.thy
@@ -298,31 +298,43 @@ proof -
     apply (erule nf)
     done
   show ?thesis
-  apply (rule corres_guard_imp)
-    apply (subst return_bind[symmetric], rule corres_split[OF P])
-      apply (rule z)
-     apply wp
-    apply (rule y)
-   apply simp+
-  done
+    apply (rule corres_guard_imp)
+      apply (subst return_bind[symmetric], rule corres_split[OF P])
+        apply (rule z)
+       apply wp
+      apply (rule y)
+     apply simp+
+    done
 qed
 
 lemmas corres_symb_exec_r_conj_ex_abs_forwards =
   corres_symb_exec_r_conj_ex_abs[where P'=P' and Q'=P' for P', simplified]
 
-lemma gets_the_corres_ex_abs:
+lemma gets_the_corres_ex_abs':
  "\<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow>
    corres_underlying sr False True r P P' (gets_the a) (gets_the b)
-   = (\<forall> s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
+   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> 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)
 
+lemmas gets_the_corres_ex_abs = gets_the_corres_ex_abs'[THEN iffD2]
+
+lemma gets_the_corres':
+ "\<lbrakk>no_ofail P a; no_ofail P' b\<rbrakk> \<Longrightarrow>
+   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
+   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
+  apply (erule gets_the_corres_ex_abs')
+  apply (fastforce intro: no_ofail_pre_imp)
+  done
+
+lemmas gets_the_corres = gets_the_corres'[THEN iffD2]
+
 lemma gets_the_corres_relation:
  "\<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f');
    P s; P' s'; (s, s') \<in> sr\<rbrakk>
   \<Longrightarrow> r (the (f s)) (the (f' s'))"
   apply (rule_tac P=P and a=f and b=f' and P'=P'
-               in gets_the_corres_ex_abs[THEN iffD1, rule_format];
+               in gets_the_corres_ex_abs'[THEN iffD1, rule_format];
          fastforce?)
   apply (rule no_ofail_gets_the_eq[THEN iffD2])
   apply (fastforce intro: corres_u_nofail)