[isabelle-dev] on the fly theorems for Isar

[Makarius]

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