*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] simplifying functions on tuples*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Wed, 27 Jan 2016 11:54:18 +0200*In-reply-to*: <56A608E1.1020508@starkeffect.com>*References*: <56A600CE.7040604@starkeffect.com> <56A606D8.3000302@inf.ethz.ch> <56A608E1.1020508@starkeffect.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

Hello, I have a certain structure F(p,f) from F_Type where p is a predicate on tuples 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

**References**:**[isabelle] "apply auto" transforms provable statement to something false?***From:*Eugene W. Stark

**Re: [isabelle] "apply auto" transforms provable statement to something false?***From:*Andreas Lochbihler

**Re: [isabelle] "apply auto" transforms provable statement to something false?***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
- Next by Date: Re: [isabelle] RC1 - Greyout
- Previous by Thread: Re: [isabelle] "apply auto" transforms provable statement to something false?
- Next by Thread: [isabelle] Goedel's paradox, canonical definitions vs. instances/models (dependent type theory and the language of species), expressiveness vs. automation, re-evaluating natural deduction
- Cl-isabelle-users January 2016 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