*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] flatten of tuples*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Fri, 27 Feb 2015 16:20:27 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <9DD7AE2D-20AA-4617-99AC-80F7309B4F8D@cam.ac.uk>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Hi Larry, Thank you for your answer. I want to model some "product of programs" in the following way: S is a program with inputs x (tuple) and v (also tuple) and outputs y (tuple) and u (tuple). S' is similar but with inputs x', v' and outputs y', u' I want the result of the product of S and S' to have input (x @ x') and (v @ v') and output (y @ y') and (u @ u'). I have a simple product S * S' that has (x,v), (x',v') as input and (y,u), (y', y') as output. If I would have the operator @, then I will define my product S ** S' as [X, V --> (x,v), (x',v') . X = (x @ x') /\ V = (v @ v')] o (S * S') o [(y,u), (y',u') --> Y,U . Y = (y @ y') /\ U = (u @ u')] Here [x,y --> a, b . P x y a b] is the nondeterministic assignment of values to a and b based on input x, y such that P x y a b is true. The programs are modeled as predicate transformers, and I can write in Isabelle the above composition almost like I have it here, except that I do not have @. Ideally the splinting of X and V in the first statement in (x @ x') and (v @ v') would be based on the type of S * S'. 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. In my case these programs are automatically generated, so in principle I know the structure of the tuples x, v, x', v' ..., so I can generate instead of the general product from above, specialized versions for the specific x, v, x', v' ... Best regards, Viorel Preoteasa On 02/27/2015 01:32 PM, Larry Paulson wrote: > An operator such as your @ seems unlikely to exist, because its operands would not have fixed types. What you mean by âsyntactic constructâ isnât clear, unless you never need to write a thing like x at y. > > I imagine that you cannot use lists because you need a variety of types. But is there is no possibility of creating a super type for them? > > Larry Paulson > > >> On 27 Feb 2015, at 02:09, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote: >> >> Hello, >> >> Is it possible to have a semantic construct which works like >> >> (a,b,c,d) @ (x,y,z) = (a,b,c,d,x,y,z) >> >> for tuples of arbitrary lengths. >> The elements a, b, ... should be of different types, >> but they are not tuples. >> >> I can also work with a version which has a terminator like: >> >> (a,b,c,d,()) @ (x,y,z,()) = (a,b,c,d,x,y,z,()) >> >> If this is not possible at the semantic level, is it possible >> to have a syntactic construct? >> >> Best regards, >> >> Viorel Preoteasa >> >>

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

**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

- Previous by Date: Re: [isabelle] change proposal: eliminating overloading for factorials
- Next by Date: Re: [isabelle] flatten of tuples
- 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