On Mon, 12 May 2014, Dmitriy Traytel wrote:
Anybody who would like to be able to quantify over type constructors in
HOL in order to reason abstractly. The command bnf_decl is a first
approximation of this: one can directly formalize statements like "for
all bounded natural functors F have ...". Of course this quantification
happens only on a meta level---no instantiation of the quantifier is
possible (without trying to resurrect the AWE tool). One example of such
a formalization is in src/HOL/BNF_Examples/Stream_Processor which
follows [1, p9, Remark].
Such axiomatizations are always a private thing, what you do behind closed
doors and don't impose on actual users.
AWE was a nice idea, because it allows to perform certain admissible rules
explicit, by replay of the proof terms. Thus it avoids the destructive
potential of arbitrary axioms, at the cost of some runtime resources for
proof term recording and replay. It is a shame that develoment of AWE
development seems to have stopped at release 0.9.1 for Isabelle 2009-1 see
also http://www.informatik.uni-bremen.de/~cxl/awe/. It is just the usual
difference of a research protoype and a tool that is released to the
general public and maintained over a long time.
With the Isabelle infrastructure of today, one could wrap up AWE nicely as
local theory target. So it might be actually worth trying to reactivate
it.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
