From f72702f2f30fd0e0ea417e82a11fad5397aee542 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 13 Jun 2023 14:05:27 +1000 Subject: [PATCH] lib: monadic rewrite: improve bound name retention MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit While in many cases using an eta form with a bind (`f >>= (λrv. g rv)`) does manage to preserve names, this was not true in general when working with monadic_rewrite. An obvious case of this was when performing a rewrite in the middle of a function, all bound variables on the way to that point would get renamed to `x`. In order to iterate over a chain of bind/bindE with a monadic_rewrite_bind_tail-style rule such that bound names are preserved, the rule's `f >>= (λrv. g rv)` must match up with the relevant bound term `do x <- f'; g' x; ...` on the RHS/LHS and only on that side: * if the rule has an eta term on both sides and the goal a schematic on any side, the schematic will match trivially producing the correct name in the first subgoal only * if the goal is not schematic and a tail rule applies, we need to choose a side to get the name from (usually the left) This means if the goal is schematic on the RHS, we need a tail rule with an eta term on its LHS, and vice-versa. Since a generic form of this is not possible, this commit introduces transformation lemmas and updates the tactics to use them for stepping on the left/right. For stopping the iteration by applying a rule to the head of a bind, the situation is reversed: to preserve the name of the bind in the tail, the head rule must not have any eta terms. The bind[E]_head rules have been updated to reflect this. Signed-off-by: Rafal Kolanski --- lib/MonadicRewrite.thy | 60 +++++++++++++++++++++++++++++++++++------- 1 file changed, 50 insertions(+), 10 deletions(-) diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index b061bf306..0269040af 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -146,18 +146,23 @@ lemma monadic_rewrite_bindE: apply (case_tac x; simp add: lift_def monadic_rewrite_refl) done +(* in order to preserve bound names in the tail, bind_head must avoid eta on both sides *) +lemma monadic_rewrite_bind_head: + "monadic_rewrite F E P f g \ monadic_rewrite F E P (f >>= h) (g >>= h)" + by (rule monadic_rewrite_bind[OF _ monadic_rewrite_refl hoare_vcg_prop, + simplified pred_top_right_neutral]) + +(* in order to preserve bound names in the tail, bindE_head must avoid eta on both sides *) +lemma monadic_rewrite_bindE_head: + "monadic_rewrite F E P f g \ monadic_rewrite F E (P and (\s. True)) (f >>=E h) (g >>=E h)" + by (rule monadic_rewrite_bindE[OF _ monadic_rewrite_refl hoare_vcg_propE_R]) + lemmas monadic_rewrite_bind_tail = monadic_rewrite_bind[OF monadic_rewrite_refl, simplified pred_top_left_neutral] -lemmas monadic_rewrite_bind_head - = monadic_rewrite_bind[OF _ monadic_rewrite_refl hoare_vcg_prop, simplified pred_top_right_neutral] - lemmas monadic_rewrite_bindE_tail = monadic_rewrite_bindE[OF monadic_rewrite_refl, simplified pred_top_left_neutral] -lemmas monadic_rewrite_bindE_head - = monadic_rewrite_bindE[OF _ monadic_rewrite_refl hoare_vcg_propE_R] - (* Same as monadic_rewrite_bind, but prove hoare triple over head of LHS instead of RHS. *) lemma monadic_rewrite_bind_l: "\ monadic_rewrite F E P f g; \x. monadic_rewrite F E (Q x) (h x) (j x); \R\ f \Q\ \ @@ -194,6 +199,36 @@ lemma monadic_rewrite_do_flip: apply (simp add: bind_assoc) done +text \control of lambda abstractions, bound variables and eta form\ + +(* Preserving bound names while iterating using bind*_tail-style rules is more complicated than + for a head-style binding: + we need an eta on the non-schematic side, and must not have an eta on the schematic side, + otherwise unification can't pick a side for name preservation automatically. + It therefore appears a generic name-preserving tail rule is not possible. + The following rules can eliminate an eta from either the LHS or RHS of a monadic_rewrite, + e.g. monadic_rewrite_bind_tail[THEN monadic_rewrite_bind_eta_r] will remove the RHS eta *) + +lemma monadic_rewrite_bind_eta_r: + "monadic_rewrite F E P f (do x <- g; h x od) + \ monadic_rewrite F E P f (g >>= h)" + by simp + +lemma monadic_rewrite_bind_eta_l: + "monadic_rewrite F E P (do x <- f; h x od) g + \ monadic_rewrite F E P (f >>= h) g" + by simp + +lemma monadic_rewrite_bindE_eta_r: + "monadic_rewrite F E P f (doE x <- g; h x odE) + \ monadic_rewrite F E P f (g >>=E h)" + by simp + +lemma monadic_rewrite_bindE_eta_l: + "monadic_rewrite F E P (doE x <- f; h x odE) g + \ monadic_rewrite F E P (f >>=E h) g" + by simp + text \catch\ lemma monadic_rewrite_catch: @@ -724,8 +759,13 @@ named_theorems monadic_rewrite_pre declare monadic_rewrite_guard_imp[monadic_rewrite_pre] method monadic_rewrite_pre = (WP_Pre.pre_tac monadic_rewrite_pre)? -method monadic_rewrite_step = - determ \rule monadic_rewrite_bind_tail monadic_rewrite_bindE_tail\ +lemmas monadic_rewrite_step_l = + monadic_rewrite_bind_tail[THEN monadic_rewrite_bind_eta_r] + monadic_rewrite_bindE_tail[THEN monadic_rewrite_bindE_eta_r] + +lemmas monadic_rewrite_step_r = + monadic_rewrite_bind_tail[THEN monadic_rewrite_bind_eta_l] + monadic_rewrite_bindE_tail[THEN monadic_rewrite_bindE_eta_l] method monadic_rewrite_solve_head methods m = (rule monadic_rewrite_bind_head monadic_rewrite_bindE_head)?, @@ -762,14 +802,14 @@ method monadic_rewrite_single_pass methods start step action finalise = (* Step over LHS until action applies, then finalise. *) method monadic_rewrite_l_method methods action finalise = monadic_rewrite_single_pass \monadic_rewrite_pre, rule monadic_rewrite_trans\ - monadic_rewrite_step + \determ \rule monadic_rewrite_step_l\\ action finalise (* Step over RHS until action applies, then finalise. *) method monadic_rewrite_r_method methods action finalise = monadic_rewrite_single_pass \monadic_rewrite_pre, rule monadic_rewrite_trans[rotated]\ - monadic_rewrite_step + \determ \rule monadic_rewrite_step_r\\ action finalise