*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] classes and interpretations*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 18 Aug 2010 16:54:59 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C6BDB13.3000506@abo.fi>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4C6BD5B1.8090805@in.tum.de> <4C6BDB13.3000506@abo.fi>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.11) Gecko/20100713 Thunderbird/3.0.6

Hi Viorel, actually, my answer is twofold: 1) > class A = ord + times + one + > assumes > .... (axioms which ensures the existence of an infimum operation) > begin > definition > "inf_l a b = ..." > end > > interpretation semilattice_inf "op <=" "op <" "inf_l"; > by ... > > The problem is now when I state some lemmas: > > lemma l1: "inf_l (a:'a::A) b <= a" > lemma (in A) l2: "inf_l a b <= a" > > The first problem is that although lemmas l1 and l2 seem similar, they > cannot > be applied in the same contexts. Lemma l2 seem more general than lemma l1. > > The second problem. The fact that inf_l is an infimum operation, given > by the > interpretation, is available when proving lemma l1, but not when > proving lemma l2. > How should I state the interpretation such that it becomes available > when proving > a lemma like l2? It seems to me that you want to use sublocale to interpret into a locale rather than into the global theory, e.g. sublocale A < prefix!: semilattice_inf "op <=" "op <" "inf_l" for an appropriate prefix (you can leave that out or make it ad libitum by leaving out the bang "!", but this is usually not recommended in the presence of pervasive interpretations to the theory level, e.g. in the case of type classes). 2) The deeper issue is the following: some algebraic structures can be specified in two different ways (let use stick with the semilattice example here) a) weak: there exists an (unique) operation such that ...; define f as some/the operation such that ... b) strong: there is an operation f such that... Once there was a decision to specify the algebraic structure type classes in the main HOL theories strong, since this is more convenient for applications, and to keep the meta-theoretic locales in HOL-Algebra weak to have them at full generality. Since what you want to do seems to be a weak specification of a semilattice, perhaps HOL-Algebra is the right environment for you. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] New AFP entry: Formalizing Statecharts using Hierarchical Automata***From:*Tobias Nipkow

**[isabelle] classes and interpretations***From:*Viorel Preoteasa

- Previous by Date: [isabelle] classes and interpretations
- Next by Date: [isabelle] Proving consistency
- Previous by Thread: [isabelle] classes and interpretations
- Next by Thread: [isabelle] Proving consistency
- Cl-isabelle-users August 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