isabelle - 伊莎贝尔有重写策略吗？

例如在 Coq 中有 rewrite，我们也可以放置箭头 `

Inductive bool: Set :=
  | true
  | false.

Lemma equality_of_functions_commutes:
  forall (f: bool->bool) x y,
    (f x) = (f y) -> (f y) = (f x).
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

来源:https://pjreddie.com/coq-tactics/#rewrite

最佳答案

我不相信它和 Coq 版本一样强大，但是

subst, described in 5.8.1 of the old tutorial 和

rewrite, shown in the examples

重写定理。但是，您不能轻易地以应用风格重写假设。

关于isabelle - 伊莎贝尔有重写策略吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/60746510/