*To*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Subject*: Re: [isabelle] flatten of tuples*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Fri, 27 Feb 2015 14:33:18 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <54F07D2B.5040601@aalto.fi>*References*: <CAHgzvFhzz3YOVMss36Jnzu+SJMpWfcH8buThYEG7HnUFzkL94w@mail.gmail.com> <54EDF0DA.3010105@inf.ethz.ch> <CAHgzvFjCA51HW3FhdgJg1ZC5GtBEyuaWmekSscTbrggeCYm8AA@mail.gmail.com> <54EE0262.6070801@inf.ethz.ch> <54EF5032.4080308@aalto.fi> <54EFD1BD.6050702@aalto.fi> <9DD7AE2D-20AA-4617-99AC-80F7309B4F8D@cam.ac.uk> <54F07D2B.5040601@aalto.fi>

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.

**Follow-Ups**:**Re: [isabelle] flatten of tuples***From:*Viorel Preoteasa

**References**:**[isabelle] Trying to instantiate a class***From:*Andrew Gacek

**Re: [isabelle] Trying to instantiate a class***From:*Andreas Lochbihler

**Re: [isabelle] Trying to instantiate a class***From:*Andrew Gacek

**Re: [isabelle] Trying to instantiate a class***From:*Andreas Lochbihler

**Re: [isabelle] Trying to instantiate a class***From:*Viorel Preoteasa

**[isabelle] flatten of tuples***From:*Viorel Preoteasa

**Re: [isabelle] flatten of tuples***From:*Larry Paulson

**Re: [isabelle] flatten of tuples***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] flatten of tuples
- Next by Date: Re: [isabelle] change proposal: eliminating overloading for factorials
- Previous by Thread: Re: [isabelle] flatten of tuples
- Next by Thread: Re: [isabelle] flatten of tuples
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list