*To*: Peter Gammie <peteg42 at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Mon, 29 Mar 2010 17:55:09 +0300*In-reply-to*: <85BA6970-0E84-407C-8840-BD6D17BE324E@gmail.com>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi> <85BA6970-0E84-407C-8840-BD6D17BE324E@gmail.com>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.8) Gecko/20100227 Thunderbird/3.0.3

Hello Peter,

case is more involved compared to the dummy example I presented in my earlier message. The locale depends actually on three type parameters: locale HoareRule = fixes pair:: "'a => 'b => ('c::order)" begin definition "SUP_L_P X u i = SUPR {v . pair v i < u} (%v . X v i)"; definition

All examples I found with locales had only one type parameter. Best regards, Viorel On 3/27/2010 2:38 PM, Peter Gammie wrote:

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

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

**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

**Re: [isabelle] Specification depends on extra type variables***From:*Peter Gammie

- Previous by Date: Re: [isabelle] Announcing I3P
- Next by Date: Re: [isabelle] Announcing I3P
- Previous by Thread: Re: [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