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.

Best wishes,

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 MHonArc.