[isabelle] Reification example fails to produce concrete representation


During my exploration of reification in Reflection_Examples.thy, I found that the it fails to produce a concrete representation for the formula in line 448 — the application of "reify" in line 449 does not produce anything. I have also tried Isabelle2017, Isabelle2018, Isabelle2019, but no such luck.

I have been informed that it might be because the occurrence of a binder and free variables. If we replace the term `x*z + 8 - y` with `x*x + x - x`, the reification produces something. But this seems unlikely since the reification works for a smaller size example e.g. ‹∀x :: int. m < 5*n - length (xs @ [2,3,4,x*z + 8 - y])›.

Does anyone know how to fix this?

Thanks in advance.


CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.

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