*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Sat, 27 Mar 2010 23:38:13 +1100*In-reply-to*: <4BACAD70.4090409@abo.fi>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi>

Viorel, On 26/03/2010, at 11:49 PM, Viorel Preoteasa wrote: > definition > f :: "'a => ('b itself) => bool" where > "f a x = (?g . !u . g (u::'b) = a)"; > > However like this I have to use x as parameter for f everywhere. > Moreover, I am defining Hoare triples for some kind of programs, > and I want to use the syntax "|- _ {| _ |} _", but with this approach > I need a place for the extra dummy parameter also. > > The fact is that the type 'b must be a type variable. I cannot instantiate it > at this point. Can I suggest you look into locales? locale L = fixes unused_x :: "'b" begin definition "f a = (?g. !u. g (u::'b) = a)" end (untested, but I can expand on this if you think it might be a profitable approach.) You can later instantiate 'b with a sublocale or interpretation command. cheers peter -- http://peteg.org/

**Follow-Ups**:**Re: [isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

**References**:**[isabelle] Antiquotation for Theorem Names***From:*Christian Sternagel

**Re: [isabelle] Antiquotation for Theorem Names***From:*Alexander Krauss

**[isabelle] Specification depends on extra type variables***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
- Next by Date: Re: [isabelle] Specification depends on extra type variables
- Previous by Thread: [isabelle] Specification depends on extra type variables
- Next by Thread: Re: [isabelle] Specification depends on extra type variables
- Cl-isabelle-users March 2010 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