[isabelle] Smash flex-flex pairs in calculational reasoning



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.