[isabelle] Usability Lifting and Transfer



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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.