Re: [isabelle] Reification example fails to produce concrete representation
I played around a bit, and while I don't understand the reason for the
problem, I managed to come up with a much smaller example that
illustrates the same(?) problem:
lemma "∀x::int. (length [y] = length [y])" for y :: int
apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
Note that when the allquantifier is remove, *or* when one of the y's is
replaced by 0, reification works. So the problem seems to be some subtle
interaction between the allquantifier and the fact that y occurs twice.
On 5/7/20 2:34 PM, Albert Rizaldi wrote:
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