[isabelle] Smash flex-flex pairs in calculational reasoning
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
Thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and