[isabelle-dev] on the fly theorems for Isar
Makarius
makarius at sketis.net
Sat Apr 17 17:41:17 CEST 2010
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
More information about the isabelle-dev
mailing list