On Sat, 17 Apr 2010, Mamoun FILALI-AMINE wrote:
Is it possible to have an "on the fly" facility for Isar:
currently we have to remember theorem names in order to reuse them
the onthefly would prove again the given theorem on the fly
example:
instead of
unfolding imp_disjL
one would write
unfolding (onthefly "(a \/ b --> c) = ((a --> c) /\ (b --> c))")
Isar only allows such implicit facts modulo unification against the
(visible) proof context. The notation is `prop` and can be used in any
position where a fact is expected, e.g. "from `prop` have XXX by blast".
In this form the proof is done via the "fact" method. I.e. the following
versions are equaivalent:
note `prop`
have "prop" by fact
Beyond the "fact" method, Isar requires explicit an explicit proof, e.g.
have *: "prop" by auto
have XXX unfolding * ...
Anyway, the example above uses 'unfolding' in a slightly non-standard way,
namely a general simplification, not unfolding of a definition. In all
these years, the Simplifier invocation behind unfolding/unfold has been a
bit too liberal in admitting many other things, while failing to unfold
definitions in certain situations where not all arguments are given. (I
wonder if it can ever be put into a form where it really unfolds
definitions reliably, no more no less.)
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
