*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] Specification depends on extra type variables*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Tue, 30 Mar 2010 10:50:29 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4BB0BF4D.9040307@abo.fi>*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>

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 -- http://peteg.org/

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

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

- Previous by Date: [isabelle] about 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