CODEWITHSUNDEEP
isabelletheorem-proving
Charlie Parker
Charlie Parker

Reputation: 5201

Is there a rewrite tactic in Isabelle?

For example in Coq there is rewrite and we can also put arrows `<-:

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.

source: https://pjreddie.com/coq-tactics/#rewrite

Upvotes: 4

Views: 399

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

I don't believe that it is as strong as the Coq version, but

rewrite theorems. However, you cannot easily rewrite assumptions in apply-style.

Upvotes: 3

Related Questions