Email Gateway (Aug 18 2022 at 18:37): Email Gateway (Aug 18 2022 at 18:37):From: Christian STERNAGEL <c-sterna@jaist.ac.jp>
I was not aware of HOL-Algebra. That looks great, thank you! Until now I
did always skip (or simply not understand) parts of the documentation
that mentioned (structure) and indices, but this looks really useful. Is
there some paper/tutorial/documentation that describes structures for
dummies? ;)
cheers
chris
Email Gateway (Aug 18 2022 at 18:47):From: Christian STERNAGEL <c-sterna@jaist.ac.jp>
Hi all,
I seem to be unable to extract the necessary information from the locale
documentation. Could somebody explain what happens in the following
declaration?
locale poset = ord +
fixes A :: "'a set"
assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y
<= x)"
and refl: "x : A ==> x <= x"
and trans: "[|x : A; y : A; z : A; x <= y; y <= z|] ==> x <= z"
My goal was to reuse the syntax of ord and define a locale capturing
partially ordered sets. However, the above declaration gives me:
print_locale poset
locale elements:
fixes less_eq :: "'a ⇒ 'a ⇒ bool"
and less :: "'a ⇒ 'a ⇒ bool"
and A :: "'b ⇒ bool"
assumes "poset A"
And I doen't see why the carrier A does not have elements of the same
type as less_eq and less? How could I achieve this effect?
cheers
chris
Email Gateway (Aug 18 2022 at 18:47):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Christian,
ord is a type class in the first place, not a pure locale. Hence, mixfix syntax
works a little differently, which interferes with parsing of the assumptions. If
ord was a standard locale that declares < and <= as notation, your declaration
would work.
locale poset = ord +
fixes A :: "'a set"
assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y <= x)"
and refl: "x : A ==> x <= x"
and trans: "[|x : A; y : A; z : A; x <= y; y <= z|] ==> x <= z"
Trying to process this declaration in Isabelle2011-1, I get an error message
saying that 'a was not of class ord. This already give some hint about the
problem. Syntax declarations in type class contexts do not arrive at the locale,
the following post mentions this:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-June/msg00045.html
Hence, Isabelle does not parse the occurrences of < and <= as the locale
parameters. Instead, it interprets them as the overloaded "constants" less and
less_eq. Consequently, A's type is not related to less' and less_eq's.
Experts on classes and locales (Florian, Clemens) might tell you why syntax is
not imported.
I don't know any satisfactory workaround. Of course, you could force the type
variables to agree by repeating less and less_eq with type signatures in a for
clause, but that would erase all notation. Equivalently, you could refrain from
mixfix syntax and literally use less and less_eq in the assumptions. Then,
Isabelle unifies the type variables. But syntax is still not available inside
the context.
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 18:47):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
the issue is that the syntax <= < is not defined in the locale ord, but
in the type class ord. Hence <= < in your spec do not refer to 'a but
to a fresh 'b::ord.
A quick solution to your issue is to turn »locale« into »class«. If
this it not suitable for your modelling, I suggest to use syntactic
variants for <= <, e.g. bended ones. Replacing or overloading standard
syntax in HOL-Main is nothing I recommend.
Btw. did you have a look at HOL-Algebra? You will also find order
specifications there which look quite similar to yours.
Florian
Last updated: Nov 21 2024 at 12:39 UTC