[isabelle-dev] bnf_decl axiomatization

[Makarius]

On Tue, 13 May 2014, Dmitriy Traytel wrote:

> Let me explain Jasmin's ";)": bnf_axiomatization was the name, I 
> intended for the command first, before I was persuaded by my colleagues 
> to correlate the name with "typedecl" rather than "axiomatization".

Odd.  We basically have this hierarchy of danger:

   * typedecl: level 0

     Totally harmless and vacous addition to the logical environment.  A
     genuine declaration that merely makes a name well-formed that was not
     known before.  Thus it is OK to have that in Pure -- there is no
     logical content yet.

   * typedef: level 1

     Slightly odd axiom scheme that is customarily called "type definition"
     in the HOL community.  In reality it does more than merely introducing
     a name for an existing item: it postulates a new type with properties
     from same vague semantic universe in the background, a type that was
     not present in the logical environment before. Thus a typedef is not
     really conservative in the strict sense, but it is OK under certain
     general assumptions how HOL is used.

   * bnf_axiomatization: level > 2

     As clearly indicated "axiomatization" it does not need to justify the
     precise level.

In the grey area > 1 there are various HOLCF domain axiomatizations that 
were tried by Franz Regensburger and David von Oheimb long before Brian 
Huffman worked on that in a more foundational way.  In the ancient times 
there were running gags like "this works thanks to categorical resoning", 
but it was unclear what the latter actually was, beyond > 50 pages of 
LaTeX in some book or thesis.  (See also 
http://www.lel.ed.ac.uk/~heycock/proof.html)


 	Makarius