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

Question

例如，在 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

Answer 1

我不相信它像 Coq 版本那么强大，但是

• subst, described in 5.8.1 of the old tutorial和

• rewrite, shown in the examples

重写定理。但是，您无法轻松地以 apply-style 重写假设。