[isabelle-dev] bnf_decl axiomatization

[Makarius]

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