isabellehol

Specifying direction of rule in Isabelle/HOL

I have found the same problem when proving several lemmas: rules with an equality sometimes only work in one direction.

For instance, I'd like to use append_assoc to get from xs @ ys @ zs to (xs @ ys) @ zs, but since append_assoc is defined as (xs @ ys) @ zs = xs @ ys @ zs, I can't.

Is there any way to indicate I want to use some rule backwards?

Thanks in advance.

Solution

  • The rule with swapped left- and right-hand sides is obtained by applying an attribute symmetric to the original rule:

    lemma "xs @ ys @ zs = (xs @ ys) @ zs"
  by (rule append_assoc [symmetric])