From 164fe2dc77791f446f3e180be5db07f53e22116a Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Fri, 18 Aug 2023 00:36:41 +0930
Subject: [PATCH] lib: small changes

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

diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy
index d8476f0125..dc80b3e22c 100644
--- a/lib/ExtraCorres.thy
+++ b/lib/ExtraCorres.thy
@@ -246,7 +246,7 @@ lemma in_whileLoop_corres:
                 "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
   and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
   and result: "(rv', t') \<in> fst (whileLoop C' B' r' s')"
-  and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
+  and nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
   shows "\<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s'
                 \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C B r s) \<and> (t, t') \<in> srel \<and> rrel rv rv')"
   apply (rule in_whileLoop_induct[OF result])
@@ -305,11 +305,11 @@ lemma whileLoop_terminates_cross:
   and cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
   and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
                 "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
-  and abs_termination: "\<And>r s. (P r s \<and> C r s) \<Longrightarrow> whileLoop_terminates C B r s"
+  and abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
   and ex_abs: "ex_abs_underlying srel (P r) s'"
   and rrel: "rrel r r'"
   and P': "P' r' s'"
-  and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
+  and nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
   shows "whileLoop_terminates C' B' r' s'"
 proof -
   have helper: "\<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s'
@@ -341,7 +341,7 @@ lemma corres_whileLoop_abs_ret:
   and body_inv: "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>\<lambda>r. P r\<rbrace>"
                 "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>\<lambda>r'. P' r'\<rbrace>"
   and abs_termination: "\<And>r s. (P r s \<and> C r s) \<Longrightarrow> whileLoop_terminates C B r s"
-  and nf: "nf \<Longrightarrow> (\<And>r. no_fail (P r and C r) (B r))"
+  and nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
   shows "corres_underlying srel nf nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')"
   apply (rule corres_underlyingI)
    apply (frule in_whileLoop_corres[OF body_corres body_inv];
@@ -378,9 +378,7 @@ lemma corres_whileLoop_abs_ret:
    apply (rename_tac abs_r)
    apply (rule no_fail_pre)
     apply (rule_tac G="rrel abs_r conc_r" in no_fail_grab_asm)
-    apply (rule corres_u_nofail)
-     apply (fastforce dest: body_corres)
-    apply (fastforce dest: nf)
+    apply (fastforce intro: corres_u_nofail dest: body_corres nf)
    apply (fastforce simp: cond)
   apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']])
   done