From fe1bbaea285ef5cb34177432d39a11cc92d3c3a2 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Thu, 18 Apr 2024 10:51:37 +1000
Subject: [PATCH] lib/monads/trace: update wp attributes to match nondet

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/trace/Trace_RG.thy  | 19 +++++++++++++++---
 lib/Monads/trace/Trace_VCG.thy | 35 +++++++++++++++++++++++++++++++---
 2 files changed, 48 insertions(+), 6 deletions(-)

diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index baff602f5b..a56cea300b 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -858,6 +858,11 @@ lemma rg_vcg_split_case_sum:
        \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>"
   by (cases x; simp)
 
+lemma rg_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validIE_def)
+  by (wp | assumption)+
+
 lemma bind_twp_nobind:
   "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> do f; g od \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>"
   by (erule bind_twp_fwd) clarsimp
@@ -1409,16 +1414,24 @@ lemmas all_rg_classic_wp_combs =
   rg_classic_wp_combs
 
 lemmas rg_wp_splits[wp_split] =
-  bind_twp bindE_twp handleE'_twp handleE_twp
+  handleE'_twp handleE_twp
   catch_twp rg_vcg_if_split rg_vcg_if_splitE
   liftM_twp liftME_twp whenE_twp unlessE_twp
   validIE_validI
 
 lemmas [wp_comb] = rg_wp_state_combsE rg_wp_combsE rg_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   bind_twp, bindE_twp and rg_seq_extE are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   rg_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] = rg_vcg_prop bind_twp bindE_twp rg_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = rg_vcg_prop
-              twp_post_taut
+lemmas [wp] = twp_post_taut
               twp_post_tautE
               rg_fun_app_twp
               liftE_twp
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index bd68d0cedd..1fc46c6daa 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -520,6 +520,24 @@ lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
 lemmas hoare_seq_ext = seq_ext[rotated]
 lemmas hoare_vcg_seqE = seqE[rotated]
 
+lemmas hoare_vcg_seqE_R = validE_validE_R[OF hoare_vcg_seqE [OF validE_R_validE validE_R_validE]]
+lemmas hoare_vcg_seqE_E = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
+
+lemma hoare_seq_extE_R:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE_E:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x -,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g -,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_E_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_def)
+  by (wp | assumption)+
+
 lemma hoare_seq_ext_nobind:
   "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>"
   by (erule seq_ext) (clarsimp simp: valid_def)
@@ -1102,7 +1120,7 @@ lemmas all_classic_wp_combs =
   hoare_classic_wp_combs
 
 lemmas hoare_wp_splits[wp_split] =
-  hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
+  handleE'_wp handleE_wp
   validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
   validE_validE_R [OF handleE'_wp [OF validE_R_validE]]
   validE_validE_R [OF handleE_wp [OF validE_R_validE]]
@@ -1114,9 +1132,20 @@ lemmas hoare_wp_splits[wp_split] =
 
 lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE  hoare_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   hoare_seq_ext, hoare_vcg_seqE and their variants are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] =
+  hoare_vcg_prop hoare_seq_ext
+  hoare_vcg_seqE_R hoare_vcg_seqE_E hoare_vcg_seqE
+  hoare_seq_extE_R hoare_seq_extE_E hoare_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = hoare_vcg_prop
-              wp_post_taut
+lemmas [wp] = wp_post_taut
               hoare_fun_app_wp
               returnOk_E
               liftE_validE_E