*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, "usr isabelle Mailinglist" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Usability Lifting and Transfer*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 22 Sep 2014 10:45:04 +0200*In-reply-to*: <541D8E4A.2000407@informatik.tu-muenchen.de>*References*: <541D8E4A.2000407@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

Hi Florian,

Andreas On 20/09/14 16:25, Florian Haftmann wrote:

Hi all, this is a elaboration raised by the thread https://groups.google.com/forum/#!topic/fa.isabelle/TmzVaYzDoGc. In my understanding the deeper reason for this situation is that currently, if you develop a specification using lift_definition, you are actually forced to use lift_definition throughout, otherwise the transfer method becomes unusable. I acknowledge that this is a consequence of the actual way of how transfer is working. On the other hand, I see two points why this is unsatisfactory. a) One of the strengths of Isabelle is that the initial definition is not that important. Indeed, as you prefer, you can establish different specificational views (primitive, equational, inductive) on operations by providing appropriate theorems (and declare them to proof tools etc. accordingly). See the attached example for different but equivalent definitions of a distinctness predicate. This gives you the freedom to switch to the »representation« which suits best your proof application. Similarly, concerning a type, there can be operations which you want to derive from more primitive ones (and use that definition in proofs also), but also be able to lift over it. Currently, you are forced to define it using lift_definition, whether you consider this »natural« or not. b) In some situations, particularly when lifting type class instances over types, you just have not the freedom of giving your own definitions. E.g. for operation like of_nat you have to prove the class assumption relative to of_nat without any possibility to use lift_definition at all. If you are very experienced you can derive and declare your own lifting rules (see e.g. src/HOL/Code_Numeral.thy), but this is really elementary. To overcome this shortcomings, just one thought. What about a statement lift_equation t1 is t2 which is almost like lift_definition but does not introduce a new operation and operates on an existing expression t1 instead. It would give the necessary proof obligations to the user and then register the appropriate transfer rules. This would enable us to write things like lift_equation ‹of_nat :: nat => integer› is ‹of_nat :: nat => int› and establish transfer relations a posteriori. Opinions? Cheers, Florian

**Follow-Ups**:**[isabelle] How to create a new algebra based on 3 valued logic***From:*Lee Martin CCNP

**References**:**[isabelle] Usability Lifting and Transfer***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Query towards pseudo constructors
- Next by Date: Re: [isabelle] PolyML "Insufficient memory" exception while building images
- Previous by Thread: [isabelle] Usability Lifting and Transfer
- Next by Thread: [isabelle] How to create a new algebra based on 3 valued logic
- Cl-isabelle-users September 2014 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