Re: [isabelle] Value Parameter for Types



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



From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Sebastian Stüber <sebastian.stueber at t-online.de>
Sent: 11 May 2019 14:17
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] Value Parameter for Types


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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.