Re: [isabelle] flatten of tuples



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.