*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Instantiating type variables within a modified definition declaration.*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Thu, 10 Nov 2016 12:36:10 +0200*In-reply-to*: <69c41820-2071-8792-6ad4-6468578cb92e@inf.ethz.ch>*References*: <CAK0o7cbmHp4Mt-tC_Os0r7GNVrDPv1EkhzLXtG9J_k-sYCX1kw@mail.gmail.com> <69c41820-2071-8792-6ad4-6468578cb92e@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hello, I am trying to introduce syntax for a definition like construct, that in addition to creating the definition, would also insatiate all type variables to a given type (bool for simplicity) For example the declaration: mydef "TestDefA a = (a = a)" will create the theorem TestDefA_def: "TestDefA (a::bool) = (a = a)" I am trying to do this in the following way: - generalize the type variables using Thm.generalize - Drule.instantiate_normalize to instantiate the schematic type to bool This works on a theorem that has been generated with Simplifier.rewrite, but it does not work when I try to apply it to the theorem within the code for creating the definition, just before Local_Theory.notes. When I try to generalize the type variables I get the error: exception THM 0 raised (line 1127 of "thm.ML"): generalize: variable free in assumptions TestDefA ?a = (?a = ?a) [TestDefA â ??.TestDef.TestDefA] While writing this I realized, that it is not enough just to change the theorem of the definition to work on bool, but I also need to change the constant to work on bool only. Attached is the theory where I try to define this new type of definition. Any help would be appreciated. Best regards, Viorel Preoteasa

theory TestDef imports Main begin end

**Follow-Ups**:**Re: [isabelle] Instantiating type variables within a modified definition declaration.***From:*Viorel Preoteasa

**References**:**[isabelle] Turning on tracing for mode inference?***From:*Mark Wassell

**Re: [isabelle] Turning on tracing for mode inference?***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Turning on tracing for mode inference?
- Next by Date: Re: [isabelle] Instantiating type variables within a modified definition declaration.
- Previous by Thread: Re: [isabelle] Turning on tracing for mode inference?
- Next by Thread: Re: [isabelle] Instantiating type variables within a modified definition declaration.
- Cl-isabelle-users November 2016 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