Email Gateway (Aug 19 2022 at 15:52): Email Gateway (Aug 19 2022 at 15:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Foo.thy
signature.asc
Email Gateway (Aug 19 2022 at 15:53):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 26 2024 at 16:20 UTC