  The refinement calculus provides a methodology for transforming an abstract
specification into a concrete implementation, by following a succession of
refinement rules. These rules have been mechanized in theorem-provers, thus
providing a formal and rigorous way to prove that a given program refines
another one. In a previous work, we have extended this mechanization for
object-oriented programs, where the memory is represented as a graph, and we
have integrated our approach within the rCOS tool, a model-driven software
development tool providing a refinement language. Hence, for any refinement
step, the tool automatically generates the corresponding proof obligations and
the user can manually discharge them, using a provided library of refinement
lemmas. In this work, we propose an approach to automate the search of possible
refinement rules from a program to another, using the rewriting tool Maude.
Each refinement rule in Maude is associated with the corresponding lemma in
Isabelle, thus allowing the tool to automatically generate the Isabelle proof
when a refinement rule can be automatically found. The user can add a new
refinement rule by providing the corresponding Maude rule and Isabelle lemma.
