0

在证明几个引理时，我发现了同样的问题：具有相等性的规则有时只在一个方向上起作用。

例如，我想使用append_assocto get from xs @ ys @ zsto (xs @ ys) @ zs，但由于append_assoc定义为(xs @ ys) @ zs = xs @ ys @ zs，我不能。

有什么方法可以表明我想向后使用一些规则？

提前致谢。

4

1 回答 1

3

symmetric通过将属性应用于原始规则来获得左右交换的规则：

lemma "xs @ ys @ zs = (xs @ ys) @ zs"
  by (rule append_assoc [symmetric])
于 2021-05-27T07:36:20.430 回答