Email Gateway (Aug 22 2022 at 14:57): Email Gateway (Aug 22 2022 at 14:57):From: Esseger <esseger@free.fr>
typedef plays very well with type classes. For instance, if I want to
define the type of Cauchy sequences in a metric space 'a, I can do it by:
typedef (overloaded) ('a::metric_space) Cauchy_seq
= "{u::(nat ⇒ 'a). ∀e>0. ∃N. ∀n≥N. ∀m≥N. dist (u n) (u m) < e}"
by (rule exI[of _ "λ_. undefined"], auto)
What I really would like to define, however, is not the set of Cauchy
sequences, but the completion of the space: I need to take a quotient,
identifying sequences that are asymptotically close. This is naturally a
quotient type, so I tried to define it as follows:
quotient_type (overloaded) ('a::metric_space) completion
= "nat ⇒ 'a" / partial: "λu v. ∀e>0. ∃N. ∀n≥N. ∀m≥N. dist (u n) (v m)
< e"
This definition is not accepted, it chokes on 'a::metric_space. Am I
missing the right syntax, or is there no way to define a quotient_type
using type classes? (Of course, I can always typedef everything by hand,
but this would be less satisfactory, by far.)
Esseger
Email Gateway (Aug 22 2022 at 14:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Esseger,
the solution should be simple: move the constraint to "nat => 'a :: …".
The issue is that »(…) completion« is suggestive Isar syntax as mimicry
of a HOL type, but of course while reading the specification there isn't
yet any type »completion«.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:57):From: Esseger <esseger@free.fr>
It works, thanks a lot!
Last updated: Apr 24 2024 at 08:20 UTC