Hernán Rajchert (Jan 24 2023 at 19:36): Hernán Rajchert (Jan 24 2023 at 19:36):If I have a goal with multiple let bindings, is there a way for me to call the simplifier with Let_def and only target a single definition?
I'd like something like this if I want to only simplify the first let
apply (simp only: Let_def(1))
or something like this to simplify by name
apply (simp only: Let_def(var_name))
apply (subst Let_def) might be what you are looking for. (subst (n) thm) to target the nth occurrence in the conclusion, (subst (asm))/(subst (asm) (n)) to target in assumptions. See also The Isabelle/Isar Reference Manual section 9.2.2. If you want more fine grained control the rewrite method from HOL-Library.Rewrite might be interesting.
Hernán Rajchert (Jan 25 2023 at 13:31):Thanks! That was exactly what I was looking for :). The rewrite method seems promising, I've accessed the source of the Rewrite module and it points me to this documentation PDF, which talks about a patsubst, was that renamed to rewrite? Is that documentation still relevant?
Kevin Kappelmann (Jan 25 2023 at 13:36):Yes. Maybe it's also enough if you look at the Examples file:
https://isabelle.in.tum.de/library/HOL/HOL-Examples/Rewrite_Examples.html
Last updated: Apr 26 2024 at 04:17 UTC