Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Value Parameter for Types


view this post on Zulip Email Gateway (Aug 22 2022 at 19:49):

From: Sebastian Stüber <sebastian.stueber@t-online.de>
Dear All,

I am trying to put as much information as possible into the signature of
my definitions.
Is it possible to give a value-parameter to a type?

For example the type of natural Numbers less or equal n:

typedef (n::nat) maxNat = "{i::nat | i. i≤n}"

n should be a parameter for the type. E.g. “5 maxNat” contains the
elements 1…5.

This would be really fun, when (simple) operations like “+” can be used
in the signature of definitions:

definition add::"n maxNat ⇒m maxNat ⇒(n+m) maxNat"

Thank you for the help,

Sebastian Stüber

view this post on Zulip Email Gateway (Aug 22 2022 at 19:49):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Sebastian,

What you are asking for here is dependent typing, which HOL does not support. There are some tricks to simulate dependent types via polymorphism (see, e.g., section 2 in https://www.cl.cam.ac.uk/~jrh13/papers/hol05.pdf), and the Isabelle/HOL type classes help even more here. But these tricks work well only in very specific cases.

I should add that, for dependent types, fun comes with a price. For example, defining functions like your add::"n maxNat ⇒m maxNat ⇒(n+m) maxNat" typically yields proof obligations to ensure the intended type is correct.

Best wishes,
Andrei


Last updated: Mar 28 2024 at 20:16 UTC