*To*: Albert Rizaldi <albert.rizaldi at ntu.edu.sg>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Reification example fails to produce concrete representation*From*: Dominique Unruh <unruh at ut.ee>*Date*: Mon, 25 May 2020 18:40:31 +0300*In-reply-to*: <SG2PR01MB335099ADB35E4E56A4505012B6A50@SG2PR01MB3350.apcprd01.prod.exchangelabs.com>*References*: <SG2PR01MB335099ADB35E4E56A4505012B6A50@SG2PR01MB3350.apcprd01.prod.exchangelabs.com>*Sender*: Dominique Unruh <d.unruh at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0

Hi,

lemma "∀x::int. (length [y] = length [y])" for y :: int apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)

Best wishes, Dominique. On 5/7/20 2:34 PM, Albert Rizaldi wrote:

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 < 5*n - length (xs @ [2,3,4,x*z + 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.

**References**:**[isabelle] Reification example fails to produce concrete representation***From:*Albert Rizaldi

- Previous by Date: [isabelle] New in the AFP: A verified algorithm for computing the Smith normal form of a matrix
- Next by Date: [isabelle] More on "References about mistakes and gaps in papers"
- Previous by Thread: [isabelle] Reification example fails to produce concrete representation
- Next by Thread: [isabelle] Strange eta-expanded "constants" in experiment environment
- Cl-isabelle-users May 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list