Discussion:
[isabelle] [noob] Classification functions as part of type definition?
(too old to reply)
Daniel Horne
2016-08-02 16:05:27 UTC
Permalink
Raw Message
Hi.

I've found myself running into a few situations where I want to define a
type as "an object of (existing type a) for which (boolean expression is
true)".


Suppose, for example, that I want to represent identifiers in a language
I'm trying to model. Naturally, I'd think of using the primitives
defined in string.thy, but as not all strings are valid identifiers, I'd
define a function such as


fun is_identifier :: "string => bool"


But thereafter I'd need to code it in lemmas as taking is_identifier as
an assumption. I'd tend to think it'd be neater to have identifier being
a type defined as "string which satisfies is_identifier", and was
wondering if there was a way to do this?


Thanks,

Daniel Horne
Peter Lammich
2016-08-02 16:24:23 UTC
Permalink
Raw Message
typedef id = "Collect is_identifier"
<proof that there is at least one identifier>

does what you want. However, there is no true subtyping, so using
the new type as string requires some manual work, which may be slightly
simplified by the lifting/transfer package.

--
Peter
Post by Daniel Horne
Hi.
I've found myself running into a few situations where I want to define a
type as "an object of (existing type a) for which (boolean expression is
true)".
Suppose, for example, that I want to represent identifiers in a language
I'm trying to model. Naturally, I'd think of using the primitives
defined in string.thy, but as not all strings are valid identifiers, I'd
define a function such as
fun is_identifier :: "string => bool"
But thereafter I'd need to code it in lemmas as taking is_identifier as
an assumption. I'd tend to think it'd be neater to have identifier being
a type defined as "string which satisfies is_identifier", and was
wondering if there was a way to do this?
Thanks,
Daniel Horne
Gergely Buday
2016-08-02 16:31:25 UTC
Permalink
Raw Message
This is called predicative subtyping in PVS.

You can define a subtype in that way in Isabelle as well but you need to prove that it is nonempty. I do not know how far you can get.

Consult the Isabelle/Isar Reference Manual for the proper type definition mechanism.

- Gergely
Post by Daniel Horne
Hi.
I've found myself running into a few situations where I want to define a
type as "an object of (existing type a) for which (boolean expression is
true)".
Suppose, for example, that I want to represent identifiers in a language
I'm trying to model. Naturally, I'd think of using the primitives
defined in string.thy, but as not all strings are valid identifiers, I'd
define a function such as
fun is_identifier :: "string => bool"
But thereafter I'd need to code it in lemmas as taking is_identifier as
an assumption. I'd tend to think it'd be neater to have identifier being
a type defined as "string which satisfies is_identifier", and was
wondering if there was a way to do this?
Thanks,
Daniel Horne
Lars Hupel
2016-08-02 21:14:05 UTC
Permalink
Raw Message
Hi Daniel,
Post by Daniel Horne
But thereafter I'd need to code it in lemmas as taking is_identifier as
an assumption. I'd tend to think it'd be neater to have identifier being
a type defined as "string which satisfies is_identifier", and was
wondering if there was a way to do this?
other people have suggested using "typedef" to introduce a new type.
There is even a way to have the system automatically coerce an
"identifier" to a "string" where one is expected by virtue of coercions.
(The other way would technically be possible but virtually useless.)

However, keep in mind that introducing a new type also requires logical
effort. For example, existing constants on strings need to be lifted to
the new type (concatenation comes to mind). Also, you need to transfer
lemmas from the base type to the subtype using the "transfer" method.

Another possibility would be to use an anonymous context:

context
fixes a b c :: string
assumes a: "is_identifier a"
assumes b: "is_identifier b"
assumes c: "is_identifier c"
begin

...

end

This gives you a block in your theory where you can use these "regular"
values as identifiers. Of course this only works when you need a fixed
number of them. If that's the case, it's the solution which is much
easier to work with. (You might also want to look into the concept of
"locales" in Isabelle if you're deciding to go down that route.)

Cheers
Lars

Loading...