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



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

On Di, 2016-08-02 at 16:58 +0100, Daniel Horne wrote:
> 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.