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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
