squash trace: rename seq_ext to bind_twp_fwd

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/trace/Trace_More_RG.thy

@@ -125,7 +125,7 @@ lemma rg_split_bind_case_sum:
              "\<And>rv. \<lbrace>S rv\<rbrace>,\<lbrace>R\<rbrace> h rv \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>"
   shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= case_sum g h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
-  apply (rule rg_seq_ext[OF _ y[unfolded validIE_def]])
+  apply (rule bind_twp[OF _ y[unfolded validIE_def]])
   apply (wpsimp wp: x split: sum.splits)
   done
 
@@ -135,7 +135,7 @@ lemma rg_split_bind_case_sumE:
   assumes y: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>S'\<rbrace>"
   shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= case_sum g h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   apply (unfold validIE_def)
-  apply (rule rg_seq_ext[OF _ y[unfolded validIE_def]])
+  apply (rule bind_twp[OF _ y[unfolded validIE_def]])
   apply (wpsimp wp: x[unfolded validIE_def] split: sum.splits)
   done
 
@@ -592,7 +592,7 @@ lemma liftM_pre_rg:
   assumes rl: "\<lbrace>\<lambda>s0 s. \<not> P s0 s \<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace> \<lambda>_ _ _. False \<rbrace>"
   shows "\<lbrace>\<lambda>s0 s. \<not> P s0 s \<rbrace>,\<lbrace>R\<rbrace> liftM f a \<lbrace>G\<rbrace>,\<lbrace> \<lambda>_ _ _. False \<rbrace>"
   unfolding liftM_def
-  apply (rule seq_ext)
+  apply (rule bind_twp_fwd)
    apply (rule rl)
   apply wp
   done

lib/Monads/trace/Trace_RG.thy

@@ -323,14 +323,8 @@ lemma bindE_twp[wp_split]:
    apply wpsimp+
   done
 
-\<comment> \<open>FIXME MC: improve naming for bind_twp vs seq_ext vs rg_seq_ext
-          existing proofs mention hoare_seq_ext a lot and seq_ext a few times\<close>
-\<comment> \<open>FIXME MC: names of seq_ext and seq_extE clash with valid equivalents\<close>
-lemmas seq_ext = bind_twp[rotated]
-lemmas seq_extE = bindE_twp[rotated]
-
-lemmas rg_seq_ext = bind_twp
-lemmas rg_seq_extE = bindE_twp
+lemmas bind_twp_fwd = bind_twp[rotated]
+lemmas bindE_twp_fwd = bindE_twp[rotated]
 
 lemma rg_TrueI[simp]:
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>_ _. \<top>\<rbrace> = prefix_closed f"
@@ -861,15 +855,15 @@ lemma rg_vcg_split_case_sum:
        \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>"
   by (cases x; simp)
 
-lemma rg_seq_ext_nobind:
+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 seq_ext) (clarsimp simp: valid_def)
+  by (erule bind_twp_fwd) clarsimp
 
-lemma rg_seq_ext_nobindE:
+lemma bindE_twp_nobind:
   "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> doE f; g odE \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
-  by (erule seq_extE) (clarsimp simp: validE_def)
+  by (erule bindE_twp_fwd) clarsimp
 
-lemmas rg_seq_ext_skip' = bind_twp[where Q=Q and Q'=Q for Q]
+lemmas bind_twp_skip = bind_twp[where Q=Q and Q'=Q for Q]
 
 lemma rg_chain:
   "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>s0 s. P' s0 s \<Longrightarrow> P s0 s; \<And>rv s0 s. Q rv s0 s \<Longrightarrow> S rv s0 s\<rbrakk>
@@ -1225,7 +1219,7 @@ lemma rg_vcg_handle_elseE:
   "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>e. \<lbrace>E' e\<rbrace>,\<lbrace>R\<rbrace> g e \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>x. \<lbrace>Q' x\<rbrace>,\<lbrace>R\<rbrace> h x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f <handle> g <else> h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   unfolding handle_elseE_def validIE_def
-  by (wpsimp wp: seq_ext | assumption | rule conjI)+
+  by (wpsimp wp: bind_twp_fwd | assumption | rule conjI)+
 
 lemma alternative_twp:
   assumes x: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
@@ -1418,7 +1412,7 @@ lemmas all_rg_classic_wp_combs =
   rg_classic_wp_combs
 
 lemmas rg_wp_splits[wp_split] =
-  rg_seq_ext rg_seq_extE handleE'_twp handleE_twp
+  bind_twp bindE_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
@@ -1668,24 +1662,24 @@ lemma rg_returnOk_tsp:
 named_theorems forward_inv_step_rules
 
 lemmas rg_forward_inv_step_nobind[forward_inv_step_rules] =
-  rg_seq_ext_nobind[where B=A and A=A for A, rotated]
+  bind_twp_nobind[where B=A and A=A for A, rotated]
 
-lemmas rg_seq_ext_skip[forward_inv_step_rules] =
-  rg_seq_ext[where Q="\<lambda>_. P" and P=P for P, rotated]
+lemmas bind_twp_fwd_skip[forward_inv_step_rules] =
+  bind_twp_fwd[where Q'="\<lambda>_. P" and P=P for P]
 
 lemmas rg_forward_inv_step_nobindE_valid[forward_inv_step_rules] =
-  rg_seq_ext_nobindE[where B=A and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
+  bindE_twp_nobind[where B=A and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
                         simplified validIE_eq_validI, rotated]
 
 lemmas rg_forward_inv_step_valid[forward_inv_step_rules] =
-  rg_seq_extE[where Q'="\<lambda>_. P" and P=P and E="\<lambda>_. Q" and Q="\<lambda>_. Q" for P Q,
-                 simplified validIE_eq_validI, rotated]
+  bindE_twp_fwd[where Q'="\<lambda>_. P" and P=P and E="\<lambda>_. Q" and Q="\<lambda>_. Q" for P Q,
+                 simplified validIE_eq_validI]
 
 lemmas rg_forward_inv_step_nobindE[forward_inv_step_rules] =
-  rg_seq_ext_nobindE[where B=A and A=A for A, rotated]
+  bindE_twp_nobind[where B=A and A=A for A, rotated]
 
-lemmas rg_seq_ext_skipE[forward_inv_step_rules] =
-  rg_seq_extE[where Q'="\<lambda>_. P" and P=P for P, rotated]
+lemmas bindE_twp_fwd_skip[forward_inv_step_rules] =
+  bindE_twp_fwd[where Q'="\<lambda>_. P" and P=P for P]
 
 method forward_inv_step uses wp simp =
   rule forward_inv_step_rules, solves \<open>wpsimp wp: wp simp: simp\<close>