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



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 

2016. aug. 2. 17:58 ezt Ãrta (Daniel Horne <d.horne at danielhorne.co.uk>):
>
> 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.