*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*: Tue, 06 Apr 2010 11:16:32 +0300*In-reply-to*: <310B13AA-C344-4A27-A9F4-30AE2D1182D0@gmail.com>*References*: <4BAB71A4.1020204@uibk.ac.at> <4BAC7B81.5090401@in.tum.de> <4BACAD70.4090409@abo.fi> <85BA6970-0E84-407C-8840-BD6D17BE324E@gmail.com> <4BB0BF4D.9040307@abo.fi> <310B13AA-C344-4A27-A9F4-30AE2D1182D0@gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Windows/20100228)

Hello Peter, Thank you again for your answer. I have finally figured out how to interpret the locale. What I needed was every easy: locale HoareRule = fixes pair::"'a => 'b => ('c::well_founded_transitive)" begin ... end

done;

which depends on more than one type.

hand when using classes things work more as I would expect them to work. Best regards, Viorel Peter Gammie wrote:

Viorel, On 30/03/2010, at 1:55 AM, Viorel Preoteasa wrote: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 Hoare_dgr :: "('b => ('u::complete_lattice)) => ('b × 'b => 'u => 'u) => ('b => 'u) => bool" ( "|- (_){| _ |}(_) " [900,0,900] 900) where "|- P {| D |} Q = (? X . (! w i j . X w i <= D(i, j) (SUP_L_P X (pair w i) j)) /\ P = SUP X /\ Q = (SUP X))" I have succeeded to develop this general theory, but I have problem instantiating it for concrete types. I need it instantiated for 'c = 'a * 'b where 'a and 'b are orders and the order on 'c is the lexicographic order. (pair a b) = (b a). I have built the lexicographic order on pairs, but I don't know how to instantiate this locale. All examples I found with locales had only one type parameter.I am bit confused by: (pair a b) = (b a) -- b does not have a function type. If you want 'a and 'b to be fixed-but-arbitrary, define another locale, e.g.: locale AB = fixes a :: "'a :: order" fixes b :: "'b :: order" and use sublocale to interpret the locales containing the lemmas of interest. There was a recent thread with subject "Locale Import" initiated by Andreas Lochbihler that clearly presents the approach. Intuitively you need to define every context (set of assumptions) you want the lemmas to work in as a locale. Note that you have to ensure that the order on 'a * 'b is the lexicographic one by examining the class instances -- you only get to define one instance per type. Hope this helps. cheers peter

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

- Previous by Date: Re: [isabelle] Imperative HOL
- Next by Date: [isabelle] Word vs WordMain
- Previous by Thread: [isabelle] PostDoc position at Uppsala University
- Next by Thread: Re: [isabelle] Specification depends on extra type variables
- Cl-isabelle-users April 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