lib: monadic rewrite: improve bound name retention

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 <rafal.kolanski@proofcraft.systems>

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 \<Longrightarrow> 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 \<Longrightarrow> monadic_rewrite F E (P and (\<lambda>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:
   "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk>
@@ -194,6 +199,36 @@ lemma monadic_rewrite_do_flip:
   apply (simp add: bind_assoc)
   done
 
+text \<open>control of lambda abstractions, bound variables and eta form\<close>
+
+(* 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)
+   \<Longrightarrow> 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
+   \<Longrightarrow> 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)
+   \<Longrightarrow> 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
+   \<Longrightarrow> monadic_rewrite F E P (f >>=E h) g"
+  by simp
+
 text \<open>catch\<close>
 
 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 \<open>rule monadic_rewrite_bind_tail monadic_rewrite_bindE_tail\<close>
+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 \<open>monadic_rewrite_pre, rule monadic_rewrite_trans\<close>
-                              monadic_rewrite_step
+                              \<open>determ \<open>rule monadic_rewrite_step_l\<close>\<close>
                               action
                               finalise
 
 (* Step over RHS until action applies, then finalise. *)
 method monadic_rewrite_r_method methods action finalise =
   monadic_rewrite_single_pass \<open>monadic_rewrite_pre, rule monadic_rewrite_trans[rotated]\<close>
-                              monadic_rewrite_step
+                              \<open>determ \<open>rule monadic_rewrite_step_r\<close>\<close>
                               action
                               finalise