Email Gateway (Aug 22 2022 at 14:19): Email Gateway (Aug 22 2022 at 14:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear list,
I have a sequence of calculational reasoning steps.
have "... f ... = ... (f some_argument)" for f
also have "some_other_subterm = ..."
finally have ... apply -
In some of the steps I have abstracted over the concrete term by reasoning with some
arbitrary f, which happens to be a function. Unfortunately, the "finally" step now
introduces a flex-flex pair in "calculation", because f is applied to some_argument on the
right-hand side of the first equation and some_other_subterm occurs in the ... part of the
first right-hand side.
The problem now is that the calculation at the end is completely unusable. Even a simple
"apply -" raises an exception (in Isabelle2016):
exception THM 0 raised (line 820 of "thm.ML"):
forall_intr: variable "f" free in assumptions
Why does also/finally not smash flex-flex pairs? Or is there some way to tell Isabelle to
eliminate them?
Thanks in advance,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC