Email Gateway (Aug 18 2022 at 15:52): Email Gateway (Aug 18 2022 at 15:52):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I am trying to use the class mechanism for a collection of algebraic
structures and I got into the following problem:
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?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 15:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
actually, my answer is twofold:
1)
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
signature.asc
Last updated: Apr 26 2024 at 01:06 UTC