Isabelle中是否存在可实现反向替换的subst类tactic？

不需要额外证明对称引理，直接用以下两种方式就能实现把P r转换成P l的需求：

• 使用 subst (sym X)：sym 会先把形如 l=r 的引理 X 反转成 r=l，再执行替换
• 使用 subst X[symmetric]：这是Isabelle更简洁的写法，通过 symmetric 属性直接调用引理的对称形式

修改你给出的示例，去掉辅助引理后可以这样写：

theorem "(λ x::nat . x) ≤ (λ x::nat . 2*x)"
  using [[simp_trace]]
  apply(rule le_funI)
  apply(subst (sym Nat.nat_mult_1))  -- 也可以替换成 apply(subst Nat.nat_mult_1[symmetric])
  apply(rule mult_le_mono1)
  apply(simp)
  done

这里Nat.nat_mult_1本身是1 * n = n，通过sym或symmetric属性反转等式方向后，subst就能把目标里的x替换成1*x，完全满足后续证明的需求。

内容的提问来源于stack exchange，提问作者alagris