Email Gateway (Aug 23 2022 at 09:05): Email Gateway (Aug 23 2022 at 09:05):From: Albert Rizaldi <albert.rizaldi@ntu.edu.sg>
Hi,
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 < 5n - length (xs @ [2,3,4,xz + 8 - y])›.
Does anyone know how to fix this?
Thanks in advance.
Best,
Albert
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.
Last updated: Nov 21 2024 at 12:39 UTC