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



Hi Daniel,

> 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




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