Re: [isabelle] classes and interpretations

Hi Viorel,

actually, my answer is twofold:

> 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).

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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.