Email Gateway (Aug 18 2022 at 19:20): Email Gateway (Aug 18 2022 at 19:20):From: Brian Huffman <huffman@in.tum.de>
On Thu, Mar 22, 2012 at 9:26 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:
Hi all,
currently there are two constants
op ^ :: "'b => nat => 'b"
op ^^ :: "'b => nat => 'b"making it a bit difficult for the user to choose the correct one in all
situations. As far as I see "op ^^" is just syntax for the overloaded
"compow". Shouldn't it be possible to unify this (and also relpow) by using
adhoc overloading, so that only one operator, e.g., "op ^" remains?
Hi Chris,
I assume that by "currently", you refer to Isabelle 2011-1. I am
therefore replying to the isabelle-users list.
Here's why "op ^" and "op ^^" are separate constants since 2009-1: "op
^^" is an ad hoc overloaded function, with a separate definition for
each type instance. On the other hand, "op ^" has a single generic
definition:
"a ^ 0 = 1"
"a ^ Suc n = a * a ^ n"
Having a single generic definition for "op ^" makes it possible to
prove generic lemmas about exponents, which are applicable to
arbitrary rings and semirings.
To come back to the subject, I'm missing "iteration" of predicates, i.e.,
what "_^^n" is on relations but for predicates ("'a => 'a => bool"). (Why
are predicates "less developed" than relations anyway?)
I think this is historical. Before the big set/predicate merge
experiment started in Isabelle 2008, predicates were not supported
very well by either the libraries or the definition tools (e.g.
"inductive" could only be used to define sets, not predicates).
Support for predicates has steadily improved since, and I see no
reason why we couldn't add "op ^^" for predicates now; I guess you're
the first to ask for it.
cheers
chris
PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with
"relpow"). In @{theory Relation} there is a typo in the lemma name
"prod_comp_bot1".
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 18 2022 at 19:20):From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 03/22/2012 06:42 PM, Brian Huffman wrote:
On Thu, Mar 22, 2012 at 9:26 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:Hi all,
currently there are two constants
op ^ :: "'b => nat => 'b"
op ^^ :: "'b => nat => 'b"making it a bit difficult for the user to choose the correct one in all
situations. As far as I see "op ^^" is just syntax for the overloaded
"compow". Shouldn't it be possible to unify this (and also relpow) by using
adhoc overloading, so that only one operator, e.g., "op ^" remains?Hi Chris,
I assume that by "currently", you refer to Isabelle 2011-1. I am
therefore replying to the isabelle-users list.
Thanks,
actually I was talking about the development version (hence the dev
list) but the situation is essentially the same in Isabelle2011-1 I
guess. By "adhoc overloading" I was referring to the theory
Adhoc_Overloading (e.g., used for do-notation) which could (I think) be
used to unify the syntax (independently from what you said about generic
lemmas) of funpow, relpow, compow, and what is more.
cheers
chris
Here's why "op ^" and "op ^^" are separate constants since 2009-1: "op
^^" is an ad hoc overloaded function, with a separate definition for
each type instance. On the other hand, "op ^" has a single generic
definition:"a ^ 0 = 1"
"a ^ Suc n = a * a ^ n"Having a single generic definition for "op ^" makes it possible to
prove generic lemmas about exponents, which are applicable to
arbitrary rings and semirings.To come back to the subject, I'm missing "iteration" of predicates, i.e.,
what "_^^n" is on relations but for predicates ("'a => 'a => bool"). (Why
are predicates "less developed" than relations anyway?)I think this is historical. Before the big set/predicate merge
experiment started in Isabelle 2008, predicates were not supported
very well by either the libraries or the definition tools (e.g.
"inductive" could only be used to define sets, not predicates).
Support for predicates has steadily improved since, and I see no
reason why we couldn't add "op ^^" for predicates now; I guess you're
the first to ask for it.
- Brian
cheers
chris
PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with
"relpow"). In @{theory Relation} there is a typo in the lemma name
"prod_comp_bot1".
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 18 2022 at 19:23):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
this won't work: Adhoc_Overloading can only disambiguate disjoint type
signatures (neglecting sort constraints). But the generic power operation
nat => 'a => 'a
and the set-relational one
nat => 'a set => 'a set
do overlap (subst 'a := 'a set).
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:23):From: Alexander Krauss <krauss@in.tum.de>
I think this isn't quite accurate.
IIRC, Adhoc_Overloading does respect sort constraints as expected, since
it runs in tandem with the normal type inference.
So the approach suggested by Chris could in fact work, with the effect that
"op ^ :: 'nat => ('a * 'a) set => ('a * 'a) set" would become "relpow"
"op ^ :: 'nat => 'a::power => 'a::power" would become "power"
"op ^ :: nat => 'a => 'a => 'a => 'a" would become "funpow"
"op ^ :: nat => 'a => 'a" without further constraints would be
ambiguous and generate an error during the term check phase.
compow would disappear and the (few) facts about it would be
duplicated for the two instances funpow and relpow.
This effectively moves the existing ad-hoc oveloading from the logic
back into the syntax layer, where it can now be handled rather smoothly.
The good thing would be that there is just one power operation (if we
forget about the reals for the moment :-) )
When introducing Adhoc_Overloading, I was aware of this possibility, but
I hesitated, because
Throwing more code into HOL-Main needs great care, especially when
syntax is involved.
The whole check/uncheck business is highly non-compositional. When
making Adhoc_Overloading part of HOL-Main, we would have to make sure
that it coexists nicely with other extensions, such as the class-related
type refinement, or coercive subtyping. I am sure there are a number of
unforeseen effects hidden here.
...and actually, the current situation is not too bad.
Alex
Last updated: Nov 21 2024 at 12:39 UTC