[isabelle] simplifying functions on tuples


I have a certain structure F(p,f) from F_Type where p is a predicate on
and f is a function on tuples with tuples as values.

I have a set of operations on F_Type that reduces to operations of
predicates and functions. For example I have a composition on
F_Type that, when applied to F(p,f) and F(p',f') reduces to:

F(p,f) comp F(p',f') = F(inf p (p' o f),  f o f')

I have also more complicated operations, and they all are
reduced to a composition of functions. The sizes of the tuples
are not fixed, and some of the operations change the
size of the tuples.

I have an expression of Fs and composition operators, and my
goal is to simplify it to F(p,f), and have p and f as simple as possible.

The main problem is that the tuples could be quite large (160 components
for some example), and simplifying functions over these tuples
seems very slow.

So far I came up with the following simplification pattern:

I use the format "\lambda (x,y,z) . (x+y, x*x, z - 1)" as the canonical
format for functions (and predicates), and whenever I compose

F(p,f) comp F(p',f')

I compute p'', and f'' in canonical form such that
F(p'', f'') = F(p,f) comp F(p',f'),
and I prove this as a theorem.

In order to compute f'', I take f o f' and I apply it to the tuple
(x,y,z,...), I simplify it and I get the theorem

(A) "/\ x y x ... . (f o f') (x,y,z,...) = some expression on x, y, z"

and from this I abstract to

(B) "f o f' = (\lambda (x,y,z, ...) . some expression on x, y, z)"

To get from (A) to (B), I construct dynamically a specific theorem for
the tuple (x,y,z,...)

The questions are:

1. Is there a more efficient representation of functions on tuples
that I can use?

2. Is it possible to get from (A) to (B) using a generic theorem?

Best regards,

Viorel Preoteasa

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