Re: [isabelle] Usability Lifting and Transfer



Hi Florian,

This sounds like a good idea. I have already got used to writing my own transfer rules for the functions that I do not want to (or cannot) define with lift_definition. An example of this can be found in the Coinductive entry in the AFP (theory TLList, lemmas TNil_transfer to tllist_all2_transfer).

However, one should be clear about which proof obligation should be presented to the user. If function f is defined in terms of g, for which there is already a transfer rule, then the transfer rule for f can often be proved by unfolding f's definition and invoking transfer_prover. Yet, transfer prover is very picky about the format of the goal statement. In particular, it does not like the ones set by lift_definition.

Another great feature would be to get parametric transfer rules by specifying parametricity theorems for either side of the transfer rule. Lift_definition currently does some clever rewriting there that is not so easily done manually when proving custom transfer rules.

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





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