Re: [isabelle] flatten of tuples



Thank you. I will check your paper.

I used in the past one single type to represent all values from
a program. It was OK, but I could not have the type
checker solve type miss matches anymore. Maybe
using hereditarily finite sets is different.

This was in PVS, using dependent types. The problem
was that dependent types could be only uninterpreted,
or subtypes of a given type.

Viorel Preoteasa

On 2/27/2015 4:33 PM, Larry Paulson wrote:
Personally, I would try to model values in your example using the hereditarily finite sets, as illustrated in my recent AFP paper and entry:

Paper: http://www.cl.cam.ac.uk/~lp15/papers/Formath/automata.pdf

AFP entry:
http://afp.sourceforge.net/entries/Finite_Automata_HF.shtml

Into this one type, you can naturally embed integers, booleans, characters, rationals, along with lists and trees built over them. You can also embed floating-point numbers, but not real numbers. Possibly that would be enough for your purposes. In the development version of the AFP, Iâve installed a file that defines a new type class, finitary, of types equipped with an embedding into HF. This is open-ended, because anything that is essentially a finite construction can be represented by a hereditarily finite set.

Larry Paulson


On 27 Feb 2015, at 14:20, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:

These programs are supposed to work with variables of different types
mixed together (real, int, nat, bool). I can create a super type of them
but then the verification of these programs will become more complicated.
Lists are also not good because I could no longer encode in the type the
number
of arguments a program expects as input.





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