[isabelle] Usability Lifting and Transfer

Hi all,

this is a elaboration raised by the thread

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

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
	  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
	  ‹of_nat :: nat => integer› is ‹of_nat :: nat => int›
and establish transfer relations a posteriori.




PGP available:

Attachment: Foo.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature

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