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, 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,

From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Sebastian Stüber <sebastian.stueber at>
Sent: 11 May 2019 14:17
To: cl-isabelle-users at
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.