[isabelle] [noob] Classification functions as part of type definition?



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





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